Program Verification with Separation Logic

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

Authors: 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

Recommendations

• Computer Science Logic
• Survey of research on program verification via separation logic
• A program construction and verification tool for separation logic
• Verification of logic programs
• scientific article; zbMATH DE number 3907752
• Program verification under weak memory consistency using separation logic
• scientific article; zbMATH DE number 868104
• scientific article; zbMATH DE number 4088902

Mathematics Subject Classification ID

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)

Cites Work

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

Cited In (10)

• Automatic Parallelization with Separation Logic
• Runtime Checking for Separation Logic
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• Title not available (Why is that?)
• Ribbon proofs for separation logic
• Reasoning About Sequences of Memory States
• Separation Logic Tutorial
• Programming Languages and Systems
• A machine-checked framework for relational separation logic
• Computer Science Logic

Uses Software

• CVC4
• Cyclist
• Infer
• Slide
• GitHub

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

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