Automata-Based Termination Proofs

DOI10.1007/978-3-642-02979-0_20MaRDI QIDQ3637353zbMATH OpenOpenAlexFDO

Authors Radu Iosif, Adam Rogalewicz

Publication date 9 July 2009

Published in Implementation and Application of Automata (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-02979-0_20

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formal languages and automata (68Q45)

Recommendations

• Automata-based termination proofs
• Proving Termination of Tree Manipulating Programs
• Proving termination of programs automatically with AProVE
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Proving termination and memory safety for programs with pointer arithmetic

Cites work

• Abstract regular tree model checking
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• Automata-based termination proofs
• Automated Verification of the Deutsch-Schorr-Waite Tree-Traversal Algorithm
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Flat Parametric Counter Automata
• scientific article; zbMATH DE number 1701751 (Why is no real title available?)
• scientific article; zbMATH DE number 177248 (Why is no real title available?)
• scientific article; zbMATH DE number 1954380 (Why is no real title available?)
• Programs with Lists Are Counter Automata
• Proving Termination of Tree Manipulating Programs
• Static Analysis
• The Büchi Complementation Saga
• The size-change principle for program termination
• Transition invariants and transition predicate abstraction for program termination
• Variance analyses from invariance analyses
• Verification, Model Checking, and Abstract Interpretation
• Verifying properties of well-founded linked lists

Cited in

(13)

• Automatizing termination proofs of recursively defined functions
• Automatically proving termination and memory safety for programs with pointer arithmetic
• Decision Procedures for Automating Termination Proofs
• Proving termination and memory safety for programs with pointer arithmetic
• Proving Termination of Tree Manipulating Programs
• Proof Pearl: The Termination Analysis of Terminator
• scientific article; zbMATH DE number 107881 (Why is no real title available?)
• Automata-based termination proofs
• Termination of algorithms over non-freely generated data types
• Automatic termination proofs with transformation orderings
• Automatic Termination Proofs for Programs with Shape-Shifting Heaps
• Tools and Algorithms for the Construction and Analysis of Systems
• Commutativity for concurrent program termination proofs

This page was built for publication: Automata-Based Termination Proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3637353)