A Program Construction and Verification Tool for Separation Logic

DOI10.1007/978-3-319-19797-5_7zbMath1432.68071arXiv1410.4439OpenAlexW789469962MaRDI QIDQ2941173

Georg Struth, Victor B. F. Gomes, Brijesh Dongol

Publication date: 27 August 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1410.4439

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) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (14)

Convolution as a Unifying Concept ⋮ Completeness of Nominal PROPs ⋮ A stone-type duality theorem for separation logic via its underlying bunched logics ⋮ Developments in concurrent Kleene algebra ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Automated Algebraic Reasoning for Collections and Local Variables with Lenses ⋮ Catoids and modal convolution algebras ⋮ Unnamed Item ⋮ Effect algebras, Girard quantales and complementation in separation logic ⋮ A Discrete Geometric Model of Concurrent Program Execution ⋮ Unnamed Item ⋮ From Proposition to Program ⋮ Building program construction and verification tools from algebraic principles ⋮ Unnamed Item

Uses Software

• Isabelle/HOL
• VeriFast
• jStar

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebraic separation logic
• Concurrent Kleene algebra and its foundations
• Algebras of modal operators and partial correctness
• Handbook of weighted automata
• Resources, concurrency, and local reasoning
• An axiomatic proof technique for parallel programs
• An algebraic construction of predicate transformers
• Isabelle/HOL. A proof assistant for higher-order logic
• Proving pointer programs in higher-order logic
• Constructing the Views Framework
• Mechanised Separation Algebra
• Transitive Separation Logic
• Views
• Effective interactive proofs for higher-order imperative programs
• On Locality and the Exchange Law for Concurrent Processes
• Algebra of Monotonic Boolean Transformers
• Modular Safety Checking for Fine-Grained Concurrency
• Tentative steps toward a development method for interfering programs
• The Logic of Bunched Implications
• Partition Theorems for Spaces of Variable Words
• Refinement Calculus
• Permission accounting in separation logic
• Convolution as a Unifying Concept
• Computer Science Logic
• On closed categories of functors
• On Hoare logic and Kleene algebra with tests

This page was built for publication: A Program Construction and Verification Tool for Separation Logic