Automata-based termination proofs

MaRDI QIDQ4610086zbMATH OpenFDO

Authors Radu Iosif, Adam Rogalewicz

Publication date 5 April 2018

zbMATH Keywords

Büchi automataformal verificationprograms with pointerstermination analysistree automata

Mathematics Subject Classification ID

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

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
• A general framework for automatic termination analysis od logic programs

Cited in

(11)

• Automatizing termination proofs of recursively defined functions
• Automata and program analysis
• An abstract interpretation framework for termination
• Decision Procedures for Automating Termination Proofs
• Proving Termination of Tree Manipulating Programs
• Proof Pearl: The Termination Analysis of Terminator
• Automata-Based Termination Proofs
• scientific article; zbMATH DE number 107881 (Why is no real title available?)
• 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

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 Q4610086)