scientific article; zbMATH DE number 1841809

zbMath0999.68045MaRDI QIDQ4783297

John C. Reynolds, Hongseok Yang, Peter W. O'Hearn

Publication date: 4 December 2002

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2142/21420001

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (88)

Program logic and equivalence in the presence of garbage collection. ⋮ Program Verification with Separation Logic ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ On Composing Finite Forests with Modal Logics ⋮ Concise Read-Only Specifications for Better Synthesis of Programs with Pointers ⋮ Local Reasoning for Global Graph Properties ⋮ A First-Order Logic with Frames ⋮ Category-theoretic structure for independence and conditional independence ⋮ Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper) ⋮ Ghost signals: verifying termination of busy waiting ⋮ Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ A logic of separating modalities ⋮ Model checking mobile ambients ⋮ Formal verification of C systems code. Structured types, separation logic and theorem proving ⋮ Automated Theorem Proving for Assertions in Separation Logic with All Connectives ⋮ Completeness for a First-Order Abstract Separation Logic ⋮ The Laws of Programming Unify Process Calculi ⋮ A Formalisation of Smallfoot in HOL ⋮ Convergence: integrating termination and abort-freedom ⋮ Generalized arrays for Stainless frames ⋮ A verifiable low-level concurrent programming model based on colored Petri nets ⋮ Revisiting concurrent separation logic ⋮ Expressiveness and complexity of graph logic ⋮ Convolution and concurrency ⋮ Separation logic and logics with team semantics ⋮ Laws of Programming for References ⋮ A semantics for concurrent separation logic ⋮ Resources, concurrency, and local reasoning ⋮ Relational separation logic ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ A Program Construction and Verification Tool for Separation Logic ⋮ Inter-process buffers in separation logic with rely-guarantee ⋮ Formally verifying exceptions for low-level code with separation logic ⋮ Concurrent weighted logic ⋮ Trace-based verification of imperative programs with I/O ⋮ A proof procedure for separation logic with inductive definitions and data ⋮ A formal C memory model for separation logic ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ Parameterized synthesis for fragments of first-order logic over data words ⋮ Effect algebras, Girard quantales and complementation in separation logic ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ Safe Modification of Pointer Programs in Refinement Calculus ⋮ Temporal property verification as a program analysis task ⋮ Verification conditions for source-level imperative programs ⋮ Iris from the ground up: A modular foundation for higher-order concurrent separation logic ⋮ Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ⋮ Lightweight Separation ⋮ Semantics and logic of object calculi ⋮ The Relationship between Separation Logic and Implicit Dynamic Frames ⋮ Verification of the Schorr-Waite Algorithm – From Trees to Graphs ⋮ Decomposing data structure commutativity proofs with \(mn\)-differencing ⋮ Partiality, State and Dependent Types ⋮ Formal verification of a C-like memory model and its uses for verifying program transformations ⋮ Verification of finite iterations over collections of variable data structures ⋮ Footprints in Local Reasoning ⋮ Highly Automated Formal Proofs over Memory Usage of Assembly Code ⋮ Separation Logic Semantics for Communicating Processes ⋮ Multimodal Separation Logic for Reasoning About Operational Semantics ⋮ Higher-Order Separation Logic in Isabelle/HOLCF ⋮ Weak updates and separation logic ⋮ The dynamic frames theory ⋮ A Resource Analysis of the π-calculus ⋮ Algebraic separation logic ⋮ Propositional Dynamic Logic with Storing, Recovering and Parallel Composition ⋮ Graphical models of separation logic ⋮ Fifty years of Hoare's logic ⋮ Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs ⋮ Frame rule for mutually recursive procedures manipulating pointers ⋮ Unifying separation logic and region logic to allow interoperability ⋮ Typing Copyless Message Passing ⋮ Unnamed Item ⋮ On Temporal and Separation Logics ⋮ A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints ⋮ Logical vs. behavioural specifications ⋮ Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq ⋮ Automatic Parallelization and Optimization of Programs by Proof Rewriting ⋮ Bottom-Up Shape Analysis ⋮ A Machine-Checked Framework for Relational Separation Logic ⋮ An adaptation-complete proof system for local reasoning about cloud storage systems ⋮ Reasoning about block-based cloud storage systems via separation logic ⋮ Separation Logic Tutorial ⋮ A Theory of Pointers for the UTP ⋮ Unnamed Item ⋮ Local Reasoning about Data Update ⋮ Manipulating Trees with Hidden Labels ⋮ Verifying Whiley programs with Boogie ⋮ Protocol combinators for modeling, testing, and execution of distributed systems

This page was built for publication: