On the \textsc{Linear Ranking} problem for integer linear-constraint loops

DOI10.1145/2429069.2429078MaRDI QIDQ2931783zbMATH OpenOpenAlexFDO

Authors Samir Genaim, Amir M. Ben-Amram

Publication date 27 November 2014

Published in Proceedings of the 40th 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/2429069.2429078

zbMATH Keywords

linear constraintsranking functionstermination

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• Ranking functions for linear-constraint loops
• The hardness of finding linear ranking functions for lasso programs
• On the linear ranking problem for simple floating-point loops
• Computer Aided Verification
• Complexity of Bradley-Manna-Sipma lexicographic ranking functions

Cited in

(18)

• On the linear ranking problem for simple floating-point loops
• Complexity of Bradley-Manna-Sipma lexicographic ranking functions
• Algebraic model checking for discrete linear dynamical systems
• \textsc{ComplexityParser}: an automatic tool for certifying poly-time complexity of Java programs
• How to find the convex hull of all integer points in a polyhedron?
• On multiphase-linear ranking functions
• Termination of single-path polynomial loop programs
• Proving termination through conditional termination
• Linear Vertex-kernels for Several Dense Ranking r -Constraint Satisfaction Problems
• The hardness of finding linear ranking functions for lasso programs
• Termination of linear loops over the integers
• Ranking Templates for Linear Loops
• Ranking functions for linear-constraint loops
• What's decidable about discrete linear dynamical systems?
• On Lexicographic Proof Rules for Probabilistic Termination
• Multiphase-linear ranking functions and their relation to recurrent sets
• On lexicographic proof rules for probabilistic termination
• Termination analysis of programs with multiphase control-flow

This page was built for publication: On the \textsc{Linear Ranking} problem for integer linear-constraint loops

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