Automated verification of shape, size and bag properties via user-defined predicates in separation logic
From MaRDI portal
Publication:436400
DOI10.1016/j.scico.2010.07.004zbMath1243.68148OpenAlexW2045388381MaRDI QIDQ436400
Huu Hai Nguyen, Wei-Ngan Chin, Shengchao Qin, Cristina David
Publication date: 20 July 2012
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.scico.2010.07.004
separation logicautomated verificationentailment checkinginductive shape predicates with size and bag properties
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Symbolic execution proofs for higher order store programs, Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper), Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms, Verification of heap manipulating programs with ordered data by extended forest automata, Disproving Inductive Entailments in Separation Logic via Base Pair Approximation, Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic, VST-Floyd: a separation logic tool to verify correctness of C programs, Verifying pointer safety for programs with unknown calls, Automated mutual induction proof in separation logic, Completeness and expressiveness of pointer program verification by separation logic, Compositional entailment checking for a fragment of separation logic, Foundations for entailment checking in quantitative separation logic, A learning-based approach to synthesizing invariants for incomplete verification engines, Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic, Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation, Nested antichains for WS1S, Automated repair of heap-manipulating programs using deductive synthesis, Lazy Automata Techniques for WS1S, Certified Reasoning with Infinity, Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure, Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure, Unnamed Item, A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints, Invariants Synthesis over a Combined Domain for Automated Program Verification, Reasoning about block-based cloud storage systems via separation logic, A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Extending separation logic with fixpoints and postponed substitution
- Isabelle/HOL. A proof assistant for higher-order logic
- Combining programming with theorem proving
- Scalable Shape Analysis for Systems Code
- Simplify: a theorem prover for program checking
- Efficient E-Matching for SMT Solvers
- Interprocedural Shape Analysis with Separated Heap Abstractions
- Simplification by Cooperating Decision Procedures
- A Transformation System for Developing Recursive Programs
- BI as an assertion language for mutable data structures
- Compositional shape analysis by means of bi-abduction
- Programming Languages and Systems
- Verifying properties of well-founded linked lists
- Automated Deduction – CADE-20
- Presburger arithmetic with bounded quantifier alternation
- Automated Verification of Shape and Size Properties Via Separation Logic
- Static Analysis
- Programming Languages and Systems
- A Theory of Pointers for the UTP
- An axiomatic basis for computer programming
- Verification, Model Checking, and Abstract Interpretation
- Verification, Model Checking, and Abstract Interpretation
- Programming Languages and Systems
- Tools and Algorithms for the Construction and Analysis of Systems
