Monotonic Abstraction for Programs with Dynamic Memory Heaps

DOI10.1007/978-3-540-70545-1_33zbMath1155.68423MaRDI QIDQ3512503

Frédéric Haziza, Ahmed Rezine, Ahmed Bouajjani, Jonathan Cederberg, Parosh Aziz Abdulla

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

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

Related Items

Monotonic Abstraction in Parameterized Verification, Programs with lists are counter automata, Well-structured graph transformation systems, 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