Proving Conditional Termination

DOI10.1007/978-3-540-70545-1_32MaRDI QIDQ3512502zbMATH OpenOpenAlexFDO

Authors Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv

Publication date 15 July 2008

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-70545-1_32

Mathematics Subject Classification ID

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

Recommendations

• Proving termination through conditional termination
• Deciding conditional termination
• Deciding conditional termination
• Syntax-guided termination analysis
• scientific article; zbMATH DE number 1903370

Cited in

(13)

• Convergence: integrating termination and abort-freedom
• Loop summarization using state and transition invariants
• Discovering non-terminating inputs for multi-path polynomial programs
• Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
• Termination of single-path polynomial loop programs
• Proving termination through conditional termination
• All-Termination(T)
• A versatile concept for the analysis of loops
• Multiphase-linear ranking functions and their relation to recurrent sets
• Inference of ranking functions for proving temporal properties by abstract interpretation
• A new look at the automatic synthesis of linear ranking functions
• On termination of polynomial programs with equality conditions
• Reflections on termination of linear loops

This page was built for publication: Proving Conditional Termination

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