Ranking Functions for Linear-Constraint Loops
From MaRDI portal
Publication:5501930
DOI10.1145/2629488zbMath1321.68296arXiv1208.4041OpenAlexW1983764301MaRDI QIDQ5501930
Samir Genaim, Amir M. Ben-Amram
Publication date: 14 August 2015
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1208.4041
Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)
Related Items
Decision tree learning in CEGIS-based termination analysis ⋮ Termination of Single-Path Polynomial Loop Programs ⋮ How to find the convex hull of all integer points in a polyhedron? ⋮ Termination of linear loops under commutative updates ⋮ What's decidable about discrete linear dynamical systems? ⋮ Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis ⋮ Time-bounded termination analysis for probabilistic programs with delays ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes ⋮ Unnamed Item ⋮ Synthesizing ranking functions for loop programs via SVM ⋮ O-Minimal Invariants for Discrete-Time Dynamical Systems ⋮ Algebraic model checking for discrete linear dynamical systems
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Some efficient solutions to the affine scheduling problem. I: One- dimensional time
- A new look at the automatic synthesis of linear ranking functions
- Cost analysis of object-oriented bytecode programs
- Some efficient solutions to the affine scheduling problem. II: Multidimensional time
- Closed-form upper bounds in static cost analysis
- On the Termination of Integer Loops
- Verification of Gap-Order Constraint Abstractions of Counter Systems
- On the linear ranking problem for integer linear-constraint loops
- Transition Invariants and Transition Predicate Abstraction for Program Termination
- Loop Summarization and Termination Analysis
- A Strongly Polynomial Algorithm to Solve Combinatorial Linear Programs
- Monotonicity Constraints for Termination in the Integer Domain
- Ranking Function Synthesis for Bit-Vector Relations
- Computing Two-Dimensional Integer Hulls
- A LIBRARY FOR DOING POLYHEDRAL OPERATIONS
- On Linear Characterizations of Combinatorial Optimization Problems
- Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
- Alternation for Termination
- Linear Ranking for Linear Lasso Programs
- The size-change principle for program termination
- Automatic numeric abstractions for heap-manipulating programs
- Ramsey vs. Lexicographic Termination Proving
- Recurrence with affine level mappings is P-time decidable for CLP
- An Improved Tight Closure Algorithm for Integer Octagonal Constraints
- Logic Programming
- Verification, Model Checking, and Abstract Interpretation
- Computer Aided Verification
- Termination of Integer Linear Programs
- CONCUR 2005 – Concurrency Theory
- Verification, Model Checking, and Abstract Interpretation
