Programs with lists are counter automata

DOI10.1007/s10703-011-0111-7zbMath1217.68059OpenAlexW1981273171MaRDI QIDQ537953

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

Publication date: 23 May 2011

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-011-0111-7

zbMATH Keywords

formal verificationbisimulationcounter automatalists with ordered dataprograms with singly-linked listssafety and termination

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Automatically proving termination and memory safety for programs with pointer arithmetic, Verification of heap manipulating programs with ordered data by extended forest automata, Counterexample Validation and Interpolation-Based Refinement for Forest Automata, The Viterbi algorithm for subsets of stochastic context-free languages, Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free, Continuous One-counter Automata

Uses Software

• TREX
• FAST

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Variance analyses from invariance analyses
• Proving Termination of Tree Manipulating Programs
• Monotonic Abstraction for Programs with Dynamic Memory Heaps
• Scalable Shape Analysis for Systems Code
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
• Programming Languages and Systems
• Shape Analysis for Composite Data Structures
• On Flat Programs with Lists
• Tools and Algorithms for the Construction and Analysis of Systems
• Foundations of Software Science and Computational Structures
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Programs with Lists Are Counter Automata
• Static Analysis
• CONCUR 2005 – Concurrency Theory
• Tools and Algorithms for the Construction and Analysis of Systems