Satisfiability modulo heap-based programs

DOI10.1007/978-3-319-41528-4_21MaRDI QIDQ4633544zbMATH OpenOpenAlexFDO

Authors Quang Loc Le, Jun Sun, Wei-Ngan Chin

Publication date 3 May 2019

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://ink.library.smu.edu.sg/sis_research/4937

zbMATH Keywords

cyclic proofsdecision proceduresinductive predicatessatisfiabilityseparation logic

Mathematics Subject Classification ID

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

Recommendations

• A decision procedure for satisfiability in separation logic with inductive predicates
• A decision procedure for separation logic in SMT
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• A decidable fragment in separation logic with inductive predicates and arithmetic
• Modular reasoning about heap paths via effectively propositional formulas

Cited in

(18)

• Compositional entailment checking for a fragment of separation logic
• A decidable fragment in separation logic with inductive predicates and arithmetic
• Compositional satisfiability solving in separation logic
• Decision procedures for region logic
• Separation logic modulo theories
• Unified reasoning about robustness properties of symbolic-heap separation logic
• Back to the future, revisiting precise program verification using SMT solvers
• Enhancing symbolic execution of heap-based programs with separation logic for test input generation
• Verifying Heap-Manipulating Programs in an SMT Framework
• A decision procedure for satisfiability in separation logic with inductive predicates
• On the adequacy of dependence-based representations for programs with heaps
• Tractability of separation logic with inductive definitions: beyond lists
• On Symbolic Heaps Modulo Permission Theories
• Structuring the verification of heap-manipulating programs
• Efficient HEX-Program Evaluation Based on Unfounded Sets
• Modular reasoning about heap paths via effectively propositional formulas
• An efficient cyclic entailment procedure in a fragment of separation logic
• Concolic testing heap-manipulating programs

This page was built for publication: Satisfiability modulo heap-based programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4633544)