Data structure specifications via local equality axioms
From MaRDI portal
Recommendations
- A shape graph logic and a shape system
- A temporal approach to specification and verification of pointer data-structures
- Data abstraction: a general framework to handle program verification of data structures
- Local reasoning about programs that alter data structures
- A logic of reachable patterns in linked data-structures
Cited in
(21)- Simpler proofs with decentralized invariants
- Data abstraction: a general framework to handle program verification of data structures
- Compositional satisfiability solving in separation logic
- Decision procedures for extensions of the theory of arrays
- Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
- Program verification with interacting analysis plugins
- Applications of hierarchical reasoning in the verification of complex systems
- Adding decision procedures to SMT solvers using axioms with triggers
- Decidability of verification of safety properties of spatial families of linear hybrid automata
- Verification of heap manipulating programs with ordered data by extended forest automata
- Towards Complete Reasoning about Axiomatic Specifications
- Verifying Heap-Manipulating Programs in an SMT Framework
- On deciding satisfiability by theorem proving with speculative inferences
- Interactive and automated proofs for graph transformations
- Certified reasoning with infinity
- Static data structure lower bounds imply rigidity
- On Local Reasoning in Verification
- On Hierarchical Reasoning in Combinations of Theories
- Verification, Model Checking, and Abstract Interpretation
- An efficient cyclic entailment procedure in a fragment of separation logic
- Proving semantical equivalence of data specifications
This page was built for publication: Data structure specifications via local equality axioms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5716590)
