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
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)
Uses Software
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