Programs with Lists Are Counter Automata

DOI10.1007/11817963_47zbMath1188.68181MaRDI 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

68P10: Searching and sorting

68Q45: Formal languages and automata

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

68P05: Data structures

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

On the complexity of resource-bounded logics, Program Verification with Separation Logic, Guiding Craig interpolation with domain-specific abstractions, Verification of multi-linked heaps, Bounded underapproximations, Proving termination of nonlinear command sequences, Programs with lists are counter automata, 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, 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 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, Beyond Shapes: Lists with Ordered Data, Automata-Based Termination Proofs

Uses Software

• TREX