Model checking for symbolic-heap separation logic with inductive predicates

DOI10.1145/2837614.2837621MaRDI QIDQ2828247zbMATH OpenOpenAlexWikidataFDO

Authors James Brotherston, Nikos Gorogiannis, Reuben N. S. Rowe, Max Kanovich

Publication date 24 October 2016

Published in Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2837614.2837621

zbMATH Keywords

complexityinductive definitionsmodel checkingprogram testingruntime verificationseparation logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Unified reasoning about robustness properties of symbolic-heap separation logic
• Symbolic Model Checking of Logics with Actions
• Symbolic model checking with rich assertional languages
• Symbolic model checking in non-Boolean domains
• Model checking for modal intuitionistic dependence logic
• scientific article; zbMATH DE number 1222405
• A symbolic semantics for abstract model checking
• Symbolic and structural model-checking
• Programming a symbolic model checker in a fully expansive theorem prover

Cited in

(12)

• Reasoning about block-based cloud storage systems via separation logic
• Automated mutual induction proof in separation logic
• Unified reasoning about robustness properties of symbolic-heap separation logic
• Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic
• Disproving inductive entailments in separation logic via base pair approximation
• A decision procedure for satisfiability in separation logic with inductive predicates
• Tractability of separation logic with inductive definitions: beyond lists
• A theory of indirection via approximation
• Runtime Checking for Separation Logic
• Completeness of cyclic proofs for symbolic heaps with inductive definitions
• The failure of cut-elimination in cyclic proof for first-order logic with inductive definitions
• Expressiveness results for an inductive logic of separated relations

Describes a project that uses

Uses Software

• Predator
• VeriFast
• SLAyer
• Cyclist
• coreStar

This page was built for publication: Model checking for symbolic-heap separation logic with inductive predicates

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