A program construction and verification tool for separation logic
From MaRDI portal
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Abstract: A principled approach to the design of program verification and con- struction tools is applied to separation logic. The control flow is modelled by power series with convolution as separating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data flow is captured by concrete store/heap models. These are linked to the separation algebra by soundness proofs. Verification conditions and transformation laws are derived by equational reasoning within the predicate transformer quantale. This separation of concerns makes an implementation in the Isabelle/HOL proof as- sistant simple and highly automatic. The resulting tool is correct by construction; it is explained on the classical linked list reversal example.
Recommendations
Cites work
- Algebra of monotonic Boolean transformers
- Algebraic separation logic
- Algebras of modal operators and partial correctness
- An algebraic construction of predicate transformers
- An axiomatic proof technique for parallel programs
- Computer Science Logic
- Concurrent Kleene algebra and its foundations
- Constructing the views framework
- Convolution as a Unifying Concept
- Effective interactive proofs for higher-order imperative programs
- Handbook of weighted automata
- scientific article; zbMATH DE number 3915644 (Why is no real title available?)
- scientific article; zbMATH DE number 46740 (Why is no real title available?)
- scientific article; zbMATH DE number 2087445 (Why is no real title available?)
- scientific article; zbMATH DE number 1841809 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Mechanised Separation Algebra
- Modular Safety Checking for Fine-Grained Concurrency
- On closed categories of functors
- On Hoare logic and Kleene algebra with tests
- On locality and the exchange law for concurrent processes
- Partition Theorems for Spaces of Variable Words
- Permission accounting in separation logic
- Proving pointer programs in higher-order logic
- Refinement Calculus
- Resources, concurrency, and local reasoning
- Tentative steps toward a development method for interfering programs
- The Logic of Bunched Implications
- Transitive Separation Logic
- Views, compositional reasoning for concurrent programs
Cited in
(18)- A stone-type duality theorem for separation logic via its underlying bunched logics
- Catoids and modal convolution algebras
- Effect algebras, Girard quantales and complementation in separation logic
- From proposition to program. Embedding the refinement calculus in Coq
- A discrete geometric model of concurrent program execution
- Developments in concurrent Kleene algebra
- Stone-type dualities for separation logics
- Unifying heterogeneous state-spaces with lenses
- Towards algebraic separation logic
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Convolution as a Unifying Concept
- Computer Science Logic
- Abstract hidden Markov models: a monadic account of quantitative information flow
- Algebraic separation logic
- Nominal string diagrams
- Program Verification with Separation Logic
- Completeness of Nominal PROPs
- Building program construction and verification tools from algebraic principles
This page was built for publication: A program construction and verification tool for separation logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2941173)
