Programs with Lists Are Counter Automata

DOI10.1007/11817963_47zbMath1188.68181OpenAlexW2487992810MaRDI QIDQ5756740

Ahmed Bouajjani, Pierre Moro, Marius Bozga, Radu Iosif, Peter Habermehl, 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

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

Related Items

Program Verification with Separation Logic, Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data, Verification of Gap-Order Constraint Abstractions of Counter Systems, Guiding Craig interpolation with domain-specific abstractions, Model-checking CTL* over flat Presburger counter systems, 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, Reasoning about sequences of memory states, Verification of gap-order constraint abstractions of counter systems, Verification of multi-linked heaps, Forest automata for verification of heap manipulation, Bounded underapproximations, Proving termination of nonlinear command sequences, Verification of qualitative \(\mathbb Z\) constraints, Programs with lists are counter automata, Quantitative separation logic and programs with lists, On the complexity of resource-bounded logics, Beyond Shapes: Lists with Ordered Data, Juggrnaut: using graph grammars for abstracting unbounded heap structures, Automata-Based Termination Proofs

Uses Software

• TREX