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

Formal languages and automata (68Q45) Data structures (68P05) Searching and sorting (68P10) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) 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)

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

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)