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
Cites work
- scientific article; zbMATH DE number 2081098 (Why is no real title available?)
- scientific article; zbMATH DE number 1841809 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- scientific article; zbMATH DE number 965572 (Why is no real title available?)
- A decision procedure for separation logic in SMT
- An axiomatic basis for computer programming
- Automated cyclic entailment proofs in separation logic
- BI as an assertion language for mutable data structures
- Compositional shape analysis by means of bi-abduction
- Deciding entailments in inductive separation logic with tree automata
- Foundations for decision problems in separation logic with general inductive predicates
- Foundations of Software Science and Computational Structures
- Linear logic
- On the almighty wand
- Programming Languages and Systems
- Programs with Lists Are Counter Automata
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- Separation and information hiding
- Shape Analysis for Composite Data Structures
- The Logic of Bunched Implications
- The monadic second-order logic of graphs. I: Recognizable sets of finite graphs
Cited in
(30)- Automatic Parallelization with Separation Logic
- Runtime Checking for Separation Logic
- Concise outlines for a complex logic: a proof outline checker for TaDA
- Separation logics and modalities: a survey
- FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
- False failure: creating failure models for separation logic
- Separation logic and abstraction
- Viper: a verification infrastructure for permission-based reasoning
- Program logics for certified compilers
- Make flows small again: revisiting the flow framework
- On temporal and separation logics
- Completeness and expressiveness of pointer program verification by separation logic
- Modular tableaux calculi for separation theories
- scientific article; zbMATH DE number 4088902 (Why is no real title available?)
- Backwards and forwards with separation logic
- Ribbon proofs for separation logic
- Separation logic modulo theories
- A decision procedure for separation logic in SMT
- Reasoning About Sequences of Memory States
- The effects of modalities in separation logics (extended abstract)
- A program construction and verification tool for separation logic
- Survey of research on program verification via separation logic
- Separation Logic Tutorial
- Relevance heuristics for program analysis
- Programming Languages and Systems
- A complete decision procedure for linearly compositional separation logic with data constraints
- Strong-separation logic
- A machine-checked framework for relational separation logic
- Modular reasoning about heap paths via effectively propositional formulas
- Computer Science Logic
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)
