Proving Termination Through Conditional Termination

DOI10.1007/978-3-662-54577-5_6zbMath1452.68046OpenAlexW2602098845MaRDI QIDQ3303892

Albert Oliveras, Cristina Borralleras, Albert Rubio, Enric Rodríguez-Carbonell, Marc Brockschmidt, Daniel Larraz

Publication date: 5 August 2020

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2117/179916

Mathematics Subject Classification ID

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

Related Items (7)

Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Reflections on termination of linear loops ⋮ Loop detection by logically constrained term rewriting ⋮ Local Search For Satisfiability Modulo Integer Arithmetic Theories ⋮ Resource Analysis driven by (Conditional) Termination Proofs ⋮ Control-Flow Refinement by Partial Evaluation, and its Application to Termination and Cost Analysis ⋮ SMT sampling via model-guided approximation

Uses Software

• ARMC
• StarExec
• Ctrl
• KITTeL

Cites Work

• Unnamed Item
• A new look at the automatic synthesis of linear ranking functions
• Conflict-driven conditional termination
• Finding recurrent sets with backward analysis and trace partitioning
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Certifying safety and termination proofs for integer transition systems
• Resource Analysis of Complex Programs with Cost Equations
• On the linear ranking problem for integer linear-constraint loops
• Policy Iteration-Based Conditional Termination and Ranking Functions
• Loop Summarization and Termination Analysis
• Proving non-termination
• Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions
• Constrained Term Rewriting tooL
• Proving Conditional Termination
• Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
• Alternation for Termination
• Ranking Templates for Linear Loops
• Termination Analysis of C Programs Using Compiler Intermediate Languages
• Non-termination Checking for Imperative Programs
• Computer Aided Verification
• Deciding Conditional Termination
• Static Analysis
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Proving Termination Through Conditional Termination