Practical methods for proving program termination

DOI10.1007/3-540-45657-0_36MaRDI QIDQ4804915zbMATH OpenFDO

Authors Michael A. Colón, Henny B. Sipma

Publication date 1 May 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2404/24040442.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• A new look at the automatic synthesis of linear ranking functions
• Computer Aided Verification
• Verification, Model Checking, and Abstract Interpretation
• Synthesis of linear ranking functions
• Ranking Functions for Size-Change Termination II

Cited in

(32)

• A complexity tradeoff in ranking-function termination proofs
• Convergence: integrating termination and abort-freedom
• Synthesizing ranking functions for loop programs via SVM
• Ranking function synthesis for bit-vector relations
• Witness to non-termination of linear programs
• Unrestricted termination and non-termination arguments for bit-vector programs
• A context-based approach to proving termination of evaluation
• Policy iteration-based conditional termination and ranking functions
• Termination graphs for Java bytecode
• Proving stabilization of biological systems
• Cyclic proofs of program termination in separation logic
• Proving Conditional Termination
• A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
• Ranking function synthesis for bit-vector relations
• Liveness by Invisible Invariants
• Proving Termination of Integer Term Rewriting
• Generating exact nonlinear ranking functions by symbolic-numeric hybrid method
• Proving termination of nonlinear command sequences
• Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs
• Proving termination by policy iteration
• Automatic verification of counter systems with ranking function
• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• An abstract domain to infer ordinal-valued ranking functions
• Ranking Abstractions
• Ranking functions for linear-constraint loops
• Computer Aided Verification
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, Model Checking, and Abstract Interpretation
• A new look at the automatic synthesis of linear ranking functions
• Decision tree learning in CEGIS-based termination analysis
• Summarization for termination: No return!
• Property-directed incremental invariant generation

This page was built for publication: Practical methods for proving program termination

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