FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science

DOI10.1007/b104325zbMath1117.03337OpenAlexW2950473912MaRDI QIDQ5465888

Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn

Publication date: 12 August 2005

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

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Related Items

Local Reasoning for Global Graph Properties, A First-Order Logic with Frames, Formal verification of C systems code. Structured types, separation logic and theorem proving, Decision Procedure for Entailment of Symbolic Heaps with Arrays, Disproving Inductive Entailments in Separation Logic via Base Pair Approximation, Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic, A Logic-Based Framework for Reasoning about Composite Data Structures, Transitive Separation Logic, A logic of reachable patterns in linked data-structures, Undecidability of Propositional Separation Logic and Its Neighbours, Verifying pointer safety for programs with unknown calls, Resources, concurrency, and local reasoning, Automated mutual induction proof in separation logic, Separation logics and modalities: a survey, Unnamed Item, A proof procedure for separation logic with inductive definitions and data, Compositional entailment checking for a fragment of separation logic, On the almighty wand, Foundations for entailment checking in quantitative separation logic, An algebraic glimpse at bunched implications and separation logic, Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic, On the Almighty Wand, Strong-separation logic, Compositional satisfiability solving in separation logic, Quantitative separation logic and programs with lists, An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures, Contributed papers. Restriction on cut in cyclic proof system for symbolic heaps, Unifying separation logic and region logic to allow interoperability, Unnamed Item, A shape graph logic and a shape system, On Temporal and Separation Logics, Automatically verifying temporal properties of pointer programs with cyclic proof, Juggrnaut: using graph grammars for abstracting unbounded heap structures, Tractable Reasoning in a Fragment of Separation Logic, On Model Checking Boolean BI, Unnamed Item, Extended transitive separation logic, On Symbolic Heaps Modulo Permission Theories, A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions