Monotonic Abstraction for Programs with Dynamic Memory Heaps

DOI10.1007/978-3-540-70545-1_33MaRDI QIDQ3512503zbMATH OpenOpenAlexFDO

Authors Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ahmed Rezine, Parosh A. 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

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

Recommendations

• Monotonic abstraction for programs with multiply-linked structures
• Monotonic abstraction for programs with multiply-linked structures
• Verification, Model Checking, and Abstract Interpretation
• Automatic numeric abstractions for heap-manipulating programs
• Logical Approaches to Computational Barriers
• Quantified Heap Invariants for Object-Oriented Programs

Cites work

• A closed-form evaluation for Datalog queries with integer (gap)-order constraints
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• Algorithmic analysis of programs with well quasi-ordered domains.
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Computer Aided Verification
• Computer Aided Verification
• CONCUR 2004 - Concurrency Theory
• scientific article; zbMATH DE number 1754582 (Why is no real title available?)
• scientific article; zbMATH DE number 1392309 (Why is no real title available?)
• Model checking of systems with many identical timed processes
• Monotonic Abstraction for Programs with Dynamic Memory Heaps
• Parameterized Verification of Infinite-State Processes with Global Conditions
• Programs with Lists Are Counter Automata
• Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
• Shape Analysis for Composite Data Structures
• Shape Analysis of Single-Parent Heaps
• Symbolic model checking with rich assertional languages
• Tools and Algorithms for the Construction and Analysis of Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• Verifying programs with unreliable channels
• Verifying properties of well-founded linked lists
• Well-structured transition systems everywhere!

Cited in

(17)

• Hierarchical shape abstraction for analysis of free list memory allocators
• Forest automata for verification of heap manipulation
• Monotonic abstraction for programs with multiply-linked structures
• Unbounded allocation in bounded heaps
• Monotonic abstraction for programs with multiply-linked structures
• Bottom-Up Shape Analysis
• Monotonic Abstraction for Programs with Dynamic Memory Heaps
• Recency-Abstraction for Heap-Allocated Storage
• Automatic Verification of Directory-Based Consistency Protocols
• Reasoning about heap manipulating programs using automata techniques
• Monotonic abstraction in parameterized verification
• Automatic numeric abstractions for heap-manipulating programs
• A semantics for procedure local heaps and its abstractions
• Programs with lists are counter automata
• Model and proof generation for heap-manipulating programs
• Well-structured graph transformation systems
• Juggrnaut: using graph grammars for abstracting unbounded heap structures

This page was built for publication: Monotonic Abstraction for Programs with Dynamic Memory Heaps

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3512503)