Monotonic Abstraction for Programs with Dynamic Memory Heaps
From MaRDI portal
Publication:3512503
DOI10.1007/978-3-540-70545-1_33zbMath1155.68423MaRDI QIDQ3512503
Parosh Aziz Abdulla, Ahmed Bouajjani, Ahmed Rezine, Frédéric Haziza, Jonathan Cederberg
Publication date: 15 July 2008
Published in: Computer Aided Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-70545-1_33
68Q60: Specification and verification (program logics, model checking, etc.)
Related Items
Monotonic Abstraction in Parameterized Verification, Programs with lists are counter automata, Forest automata for verification of heap manipulation, Bottom-Up Shape Analysis, Monotonic Abstraction for Programs with Dynamic Memory Heaps, Automatic Verification of Directory-Based Consistency Protocols
Cites Work
- Unnamed Item
- Unnamed Item
- A closed-form evaluation for Datalog queries with integer (gap)-order constraints
- Model checking of systems with many identical timed processes
- Algorithmic analysis of programs with well quasi-ordered domains.
- Verifying programs with unreliable channels
- Monotonic Abstraction for Programs with Dynamic Memory Heaps
- Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
- CONCUR 2004 - Concurrency Theory
- Computer Aided Verification
- Computer Aided Verification
- Verifying properties of well-founded linked lists
- Parameterized Verification of Infinite-State Processes with Global Conditions
- Shape Analysis for Composite Data Structures
- Shape Analysis of Single-Parent Heaps
- Tools and Algorithms for the Construction and Analysis of Systems
- Verification, Model Checking, and Abstract Interpretation
- Automatic Termination Proofs for Programs with Shape-Shifting Heaps
- Programs with Lists Are Counter Automata
- Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
- Tools and Algorithms for the Construction and Analysis of Systems
- Well-structured transition systems everywhere!
- Symbolic model checking with rich assertional languages
