Automated mutual explicit induction proof in separation logic

DOI10.1007/978-3-319-48989-6_40zbMath1427.68350arXiv1609.00919OpenAlexW2512685755MaRDI QIDQ2281658

Siau-Cheng Khoo, Ton Chanh Le, Wei-Ngan Chin, Quang-Trung Ta

Publication date: 3 January 2020

Full work available at URL: https://arxiv.org/abs/1609.00919

Mathematics Subject Classification ID

Logic in computer science (03B70) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

A First-Order Logic with Frames ⋮ Automated mutual induction proof in separation logic ⋮ An efficient cyclic entailment procedure in a fragment of separation logic ⋮ Automated repair of heap-manipulating programs using deductive synthesis ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions

Uses Software

• z3
• Infer

This page was built for publication: Automated mutual explicit induction proof in separation logic