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

complexitymodel checkingruntime verificationseparation logicinductive definitionsprogram testing

Mathematics Subject Classification ID

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

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)

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

Describes a project that uses

Uses Software

• coreStar
• Cyclist
• SLAyer
• VeriFast
• Predator

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)