Program Verification with Separation Logic

DOI10.1007/978-3-319-94111-0_3OpenAlexW2808485914MaRDI QIDQ5883571

Radu Iosif

Publication date: 21 March 2023

Published in: Model Checking Software (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-94111-0_3

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• CVC4
• Cyclist
• Infer
• GitHub
• Slide

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On the almighty wand
• Linear logic
• A decision procedure for separation logic in SMT
• The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• Separation and information hiding
• Deciding Entailments in Inductive Separation Logic with Tree Automata
• The Logic of Bunched Implications
• BI as an assertion language for mutable data structures
• Automated Cyclic Entailment Proofs in Separation Logic
• Compositional Shape Analysis by Means of Bi-Abduction
• Foundations for Decision Problems in Separation Logic with General Inductive Predicates
• Shape Analysis for Composite Data Structures
• Programming Languages and Systems
• An axiomatic basis for computer programming
• Foundations of Software Science and Computational Structures
• Programs with Lists Are Counter Automata

This page was built for publication: Program Verification with Separation Logic