Multiphase-linear ranking functions and their relation to recurrent sets

DOI10.1007/978-3-030-32304-2_22MaRDI QIDQ6536301zbMATH OpenFDO

Authors Amir M. Ben-Amram, Jesús J. Doménech, Samir Genaim

Publication date 19 April 2024

Full work available at URL https://doi.org/10.1007/978-3-030-32304-2_22

Mathematics Subject Classification ID

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

Recommendations

• On multiphase-linear ranking functions
• Ranking functions for linear-constraint loops
• On the \textsc{Linear Ranking} problem for integer linear-constraint loops
• Termination analysis of programs with multiphase control-flow
• Automata, Languages and Programming

Cites work

• An abstract domain to infer ordinal-valued ranking functions
• An abstract interpretation framework for termination
• Automated Technology for Verification and Analysis
• Computer Aided Verification
• Computer Aided Verification
• Deciding conditional termination
• Finding recurrent sets with backward analysis and trace partitioning
• Geometric nontermination arguments
• scientific article; zbMATH DE number 1701751 (Why is no real title available?)
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• scientific article; zbMATH DE number 3336831 (Why is no real title available?)
• Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs
• Non-termination Checking for Imperative Programs
• On multiphase-linear ranking functions
• Polyhedral approaches to mixed integer linear programming
• Proving Conditional Termination
• Proving non-termination
• Proving termination through conditional termination
• Proving that programs eventually do something good
• Ranking functions for linear-constraint loops
• Ranking Templates for Linear Loops
• Some efficient solutions to the affine scheduling problem. I: One- dimensional time
• Verification, Model Checking, and Abstract Interpretation

Cited in

(5)

• Termination analysis of programs with multiphase control-flow
• The 2-dimensional constraint loop problem is decidable
• Termination of triangular polynomial loops
• Polynomial loops: beyond termination
• Targeting completeness: automated complexity analysis of integer programs

This page was built for publication: Multiphase-linear ranking functions and their relation to recurrent sets

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