Tools and Algorithms for the Construction and Analysis of Systems

DOI10.1007/11691372zbMath1180.68112OpenAlexW2739785336MaRDI QIDQ5899065

Dino Distefano, Hongseok Yang, Peter W. O'Hearn

Publication date: 2 May 2007

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

Full work available at URL: https://doi.org/10.1007/11691372

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Symbolic execution proofs for higher order store programs, Model checking dynamic memory allocation in operating systems, A Formalisation of Smallfoot in HOL, Lightweight shape analysis based on physical types, Verifying pointer safety for programs with unknown calls, Separation logics and modalities: a survey, Specifying graph languages with type graphs, Conjunctive Abstract Interpretation Using Paramodulation, Monotonic Abstraction for Programs with Dynamic Memory Heaps, An algebraic glimpse at bunched implications and separation logic, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, Unnamed Item, From Separation Logic to Hyperedge Replacement and Back, Lightweight Separation, Interprocedural shape analysis using separation logic-based transformer summaries, Verify heaps via unified model checking, Proving linearizability with temporal logic, Automated Cyclic Entailment Proofs in Separation Logic, Matching Logic: An Alternative to Hoare/Floyd Logic, Unifying separation logic and region logic to allow interoperability, On Temporal and Separation Logics, Quantified data automata for linear data structures: a register automaton model with applications to learning invariants of programs manipulating arrays and lists, A relational shape abstract domain, Automatic Parallelization and Optimization of Programs by Proof Rewriting, An adaptation-complete proof system for local reasoning about cloud storage systems, Invariants Synthesis over a Combined Domain for Automated Program Verification, Separation Logic Tutorial, Linear capabilities for fully abstract compilation of separation-logic-verified code, Local higher-order fixpoint iteration