Programs with Lists Are Counter Automata
DOI10.1007/11817963_47zbMATH Open1188.68181OpenAlexW2487992810MaRDI QIDQ5756740FDOQ5756740
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
Recommendations
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)
Cited In (27)
- 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
- Verifying properties of well-founded linked lists
- Verification of qualitative \(\mathbb Z\) constraints
- Towards Model-Checking Programs with Lists
- Guiding Craig interpolation with domain-specific abstractions
- Bounded underapproximations
- 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
- Title not available (Why is that?)
Uses Software
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)
