An abstract interpretation framework for termination

DOI10.1145/2103656.2103687MaRDI QIDQ2942877zbMATH OpenOpenAlexFDO

Authors Patrick Cousot, Radhia Cousot

Publication date 11 September 2015

Published in Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2103656.2103687

zbMATH Keywords

verificationabstract interpretationinductionstatic analysisterminationsafetyvariant function

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1696776
• The size-change principle for program termination
• Logic Programming
• Automata-based termination proofs
• Proving termination by policy iteration

Cited in

(9)

• Reflections on termination of linear loops
• Proving guarantee and recurrence temporal properties by abstract interpretation
• Proving termination by policy iteration
• Predicate abstraction for program verification
• Logic Programming
• Inferring sufficient conditions with backward polyhedral under-approximations
• Temporal prophecy for proving temporal properties of infinite-state systems
• Multiphase-linear ranking functions and their relation to recurrent sets
• Inference of ranking functions for proving temporal properties by abstract interpretation

This page was built for publication: An abstract interpretation framework for termination

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