BI as an assertion language for mutable data structures

DOI10.1145/360204.375719zbMath1323.68077OpenAlexW4256027310MaRDI QIDQ5178870

Publication date: 17 March 2015

Published in: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/360204.375719

Mathematics Subject Classification ID

Theory of programming languages (68N15) Logic in computer science (03B70) Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Bunched sequential information, Extending separation logic with fixpoints and postponed substitution, Convolution as a Unifying Concept, Program logic and equivalence in the presence of garbage collection., Program Verification with Separation Logic, On Composing Finite Forests with Modal Logics, Completeness for recursive procedures in separation logic, A stone-type duality theorem for separation logic via its underlying bunched logics, A logic of separating modalities, Model checking mobile ambients, Certifying low-level programs with hardware interrupts and preemptive threads, Formal verification of C systems code. Structured types, separation logic and theorem proving, Bringing Order to the Separation Logic Jungle, A Unified Display Proof Theory for Bunched Logic, An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics, Types, Maps and Separation Logic, Automated theorem proving by resolution in non-classical logics, A perspective on specifying and verifying concurrent modules, A calculus and logic of resources and processes, A logic of reachable patterns in linked data-structures, Undecidability of Propositional Separation Logic and Its Neighbours, Formal verification of concurrent programs with Read-write locks, Separation logic and logics with team semantics, Relational separation logic, Coalgebraic completeness-via-canonicity for distributive substructural logics, Separation logic with one quantified variable, An Epistemic Separation Logic, Separation logics and modalities: a survey, Formally verifying exceptions for low-level code with separation logic, Adjunct Elimination in Context Logic for Trees, Completeness and expressiveness of pointer program verification by separation logic, Concurrent weighted logic, Compositional entailment checking for a fragment of separation logic, Bunched logics displayed, An efficient cyclic entailment procedure in a fragment of separation logic, An epistemic separation logic with action models, A separation logic with histories of epistemic actions as resources, On the almighty wand, An undecidability result for separation logic with theory reasoning, Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic, Foundations for entailment checking in quantitative separation logic, A fine-grained semantics for arrays and pointers under weak memory models, An algebraic glimpse at bunched implications and separation logic, A calculus and logic of bunched resources and processes, Reasoning about sequences of memory states, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, Structural operational semantics through context-dependent behaviour, A public announcement separation logic, Iris from the ground up: A modular foundation for higher-order concurrent separation logic, The Essence of Higher-Order Concurrent Separation Logic, A Higher-Order Logic for Concurrent Termination-Preserving Refinement, On the Almighty Wand, A Spatial Equational Logic for the Applied π-Calculus, Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation, The Relationship between Separation Logic and Implicit Dynamic Frames, Strong-separation logic, Automated repair of heap-manipulating programs using deductive synthesis, Compositional satisfiability solving in separation logic, Entailment is undecidable for symbolic heap separation logic formulæ with non-established inductive rules, Footprints in Local Reasoning, Verify heaps via unified model checking, Unnamed Item, Interprocedural Shape Analysis for Effectively Cutpoint-Free Programs, Separation Logic for Multiple Inheritance, Multimodal Separation Logic for Reasoning About Operational Semantics, Reasoning about B+ Trees with Operational Semantics and Separation Logic, Adjunct elimination in context logic for trees, Algebra and logic for access control, Algebraic separation logic, Quantitative separation logic and programs with lists, Unnamed Item, Unnamed Item, A type system with usage aspects, An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures, Frame rule for mutually recursive procedures manipulating pointers, Certified Reasoning with Infinity, Unifying separation logic and region logic to allow interoperability, On Temporal and Separation Logics, Unnamed Item, Unifying decidable entailments in separation logic with inductive definitions, Tractable Reasoning in a Fragment of Separation Logic, Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding, A Substructural Epistemic Resource Logic, A Machine-Checked Framework for Relational Separation Logic, Fine-grained concurrency with separation logic, Possible worlds and resources: The semantics of \(\mathbf{BI}\), An adaptation-complete proof system for local reasoning about cloud storage systems, Invariants Synthesis over a Combined Domain for Automated Program Verification, Separation Logic Contracts for a Java-Like Language with Fork/Join, A Theory of Pointers for the UTP, Unnamed Item, Unnamed Item, Local Reasoning about Data Update, Systems Modelling via Resources and Processes: Philosophy, Calculus, Semantics, and Logic, On the relation between concurrent separation logic and concurrent Kleene algebra, Two decades of automatic amortized resource analysis, A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions