An abstract interpretation framework for termination

DOI10.1145/2103656.2103687zbMATH Open1321.68190OpenAlexW4240185672MaRDI QIDQ2942877FDOQ2942877

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

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

zbMATH Keywords

verificationabstract interpretationinductionstatic analysisterminationsafetyvariant function

Mathematics Subject Classification ID

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

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)