Formalised Inductive Reasoning in the Logic of Bunched Implications

DOI10.1007/978-3-540-74061-2_6zbMath1211.68081OpenAlexW2123056643MaRDI QIDQ3611996

James Brotherston

Publication date: 3 March 2009

Published in: Static Analysis (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74061-2_6

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Disproving Inductive Entailments in Separation Logic via Base Pair Approximation, Automated mutual induction proof in separation logic, Completeness and expressiveness of pointer program verification by separation logic, Automated Cyclic Entailment Proofs in Separation Logic, Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps, Unifying separation logic and region logic to allow interoperability, Automatically verifying temporal properties of pointer programs with cyclic proof, Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent, Non-well-founded deduction for induction and coinduction, Integrating induction and coinduction via closure operators and proof cycles, A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions