Programs with Lists Are Counter Automata

DOI10.1007/11817963_47MaRDI QIDQ5756740zbMATH OpenOpenAlexFDO

Authors Ahmed Bouajjani, Marius Bozga, Peter Habermehl, Radu Iosif, Pierre Moro, Tomáš Vojnar

Publication date 5 September 2007

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11817963_47

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Data structures (68P05) Searching and sorting (68P10) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Programs with lists are counter automata
• Towards Model-Checking Programs with Lists
• Tools and Algorithms for the Construction and Analysis of Systems
• On Flat Programs with Lists
• Forest automata for verification of heap manipulation

Cited in

(27)

• Verification of gap-order constraint abstractions of counter systems
• Forest automata for verification of heap manipulation
• Abstract domains for automated reasoning about list-manipulating programs with infinite data
• Verification of gap-order constraint abstractions of counter systems
• Model-checking \(\mathrm{CTL}^*\) over flat Presburger counter systems
• Guiding Craig interpolation with domain-specific abstractions
• A Logic-Based Framework for Reasoning about Composite Data Structures
• Reachability in Succinct and Parametric One-Counter Automata
• Monotonic Abstraction for Programs with Dynamic Memory Heaps
• Refinement-Based Verification for Possibly-Cyclic Lists
• Beyond Shapes: Lists with Ordered Data
• Automata-Based Termination Proofs
• Towards Model-Checking Programs with Lists
• Verification of multi-linked heaps
• scientific article; zbMATH DE number 1948389 (Why is no real title available?)
• Bounded underapproximations
• Proving termination of nonlinear command sequences
• Verifying properties of well-founded linked lists
• Programs with lists are counter automata
• On Flat Programs with Lists
• Tools and Algorithms for the Construction and Analysis of Systems
• Program Verification with Separation Logic
• On the complexity of resource-bounded logics
• Reasoning about sequences of memory states
• Quantitative separation logic and programs with lists
• Juggrnaut: using graph grammars for abstracting unbounded heap structures
• Verification of qualitative \(\mathbb Z\) constraints

Describes a project that uses

Uses Software

• TREX

This page was built for publication: Programs with Lists Are Counter Automata

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