Ramsey versus lexicographic termination proving

DOI10.1007/978-3-642-36742-7_4MaRDI QIDQ5326314zbMATH OpenOpenAlexFDO

Authors Byron Cook, Abigail See, Florian Zuleger

Publication date 5 August 2013

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-36742-7_4

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• Ranking Functions for Size-Change Termination II
• Maximal Termination
• Orderings and Constraints: Theory and Practice of Proving Termination
• On Lexicographic Proof Rules for Probabilistic Termination

Cited in

(11)

• Convergence: integrating termination and abort-freedom
• Temporal prophecy for proving temporal properties of infinite-state systems
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Stop when you are almost-full. Adventures in constructive termination
• Predicate abstraction for program verification
• Termination of single-path polynomial loop programs
• scientific article; zbMATH DE number 7559471 (Why is no real title available?)
• Ranking functions for linear-constraint loops
• On Lexicographic Proof Rules for Probabilistic Termination
• On lexicographic proof rules for probabilistic termination
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification

This page was built for publication: Ramsey versus lexicographic termination proving

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