Model checking for symbolic-heap separation logic with inductive predicates

DOI10.1145/2837614.2837621zbMath1347.68221OpenAlexW2284409231MaRDI QIDQ2828247

Nikos Gorogiannis, James Brotherston, Reuben N. S. Rowe, Max I. 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

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

Related Items

Disproving Inductive Entailments in Separation Logic via Base Pair Approximation, Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic, Automated mutual induction proof in separation logic, Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic, Unnamed Item, Reasoning about block-based cloud storage systems via separation logic

Uses Software

• Predator
• VeriFast
• SLAyer
• Cyclist
• coreStar