Linear ranking with reachability

DOI10.1007/11513988_48MaRDI QIDQ5716591zbMATH OpenOpenAlexFDO

Authors Aaron R. Bradley, Zohar Manna, Henny B. Sipma

Publication date 10 January 2006

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

Full work available at URL https://doi.org/10.1007/b138445

Mathematics Subject Classification ID

Theory of software (68N99) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Verification, Model Checking, and Abstract Interpretation
• A new look at the automatic synthesis of linear ranking functions
• Ranking functions for linear-constraint loops
• Synthesis of linear ranking functions
• Practical methods for proving program termination

Cited in

(39)

• Convergence: integrating termination and abort-freedom
• On the linear ranking problem for simple floating-point loops
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Synthesizing ranking functions for loop programs via SVM
• \textsc{LTL} falsification in infinite-state systems
• On multiphase-linear ranking functions
• Ranking function synthesis for bit-vector relations
• Witness to non-termination of linear programs
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Synthesis of linear ranking functions
• Lower runtime bounds for integer programs
• On the \textsc{Linear Ranking} problem for integer linear-constraint loops
• Termination of single-path polynomial loop programs
• Proving termination through conditional termination
• Detection of ranking functions of polynomial loop programs
• A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing Analysis
• Ranking function synthesis for bit-vector relations
• Proving Termination of Integer Term Rewriting
• scientific article; zbMATH DE number 4072701 (Why is no real title available?)
• Practical methods for proving program termination
• The hardness of finding linear ranking functions for lasso programs
• scientific article; zbMATH DE number 7453196 (Why is no real title available?)
• Linear ranking for linear lasso programs
• A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
• SVM-based method for detecting ranking functions in polynomial loop programs
• Ranking Templates for Linear Loops
• Ranking functions for linear-constraint loops
• Verification, Model Checking, and Abstract Interpretation
• Constraint solving for interpolation
• MDPs as distribution transformers: affine invariant synthesis for safety objectives
• 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
• Termination of triangular polynomial loops
• A new look at the automatic synthesis of linear ranking functions
• Proving mutual termination
• Reflections on termination of linear loops
• Decision tree learning in CEGIS-based termination analysis
• Property-directed incremental invariant generation

This page was built for publication: Linear ranking with reachability

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