Program Verification with Separation Logic

DOI10.1007/978-3-319-94111-0_3MaRDI QIDQ5883571OpenAlexFDO

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

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)

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)

• Make flows small again: revisiting the flow framework
• Separation logics and modalities: a survey
• scientific article; zbMATH DE number 4088902 (Why is no real title available?)
• Modular reasoning about heap paths via effectively propositional formulas
• Programming Languages and Systems
• A program construction and verification tool for separation logic
• Runtime Checking for Separation Logic
• Completeness and expressiveness of pointer program verification by separation logic
• Relevance heuristics for program analysis
• A machine-checked framework for relational separation logic
• Concise outlines for a complex logic: a proof outline checker for TaDA
• Modular tableaux calculi for separation theories
• False failure: creating failure models for separation logic
• Ribbon proofs for separation logic
• Separation logic modulo theories
• Separation logic and abstraction
• Separation Logic Tutorial
• Survey of research on program verification via separation logic
• A complete decision procedure for linearly compositional separation logic with data constraints
• Reasoning About Sequences of Memory States
• Program logics for certified compilers
• FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science
• A decision procedure for separation logic in SMT
• Viper: a verification infrastructure for permission-based reasoning
• Backwards and forwards with separation logic
• The effects of modalities in separation logics (extended abstract)
• Computer Science Logic
• On temporal and separation logics
• Automatic Parallelization with Separation Logic
• Strong-separation logic

Describes a project that uses

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)