Proving termination through conditional termination
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- A new look at the automatic synthesis of linear ranking functions
- Alternation for termination
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Certifying safety and termination proofs for integer transition systems
- Computer Aided Verification
- Conflict-driven conditional termination
- Constrained term rewriting tooL
- Deciding conditional termination
- Finding recurrent sets with backward analysis and trace partitioning
- Loop Summarization and Termination Analysis
- Minimal-model-guided approaches to solving polynomial constraints and extensions
- Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs
- Non-termination Checking for Imperative Programs
- On the \textsc{Linear Ranking} problem for integer linear-constraint loops
- Policy iteration-based conditional termination and ranking functions
- Proving Conditional Termination
- Proving non-termination
- Ranking Templates for Linear Loops
- Resource analysis of complex programs with cost equations
- Static Analysis
- Termination Analysis of C Programs Using Compiler Intermediate Languages
- Verification, Model Checking, and Abstract Interpretation
Cited in
(16)- Control-flow refinement by partial evaluation, and its application to termination and cost analysis
- Proving Conditional Termination
- Term Rewriting and Applications
- Reflections on termination of linear loops
- Loop detection by logically constrained term rewriting
- Conflict-driven conditional termination
- Alternation for termination
- SMT sampling via model-guided approximation
- Resource analysis driven by (conditional) termination proofs
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Proving Non-Termination by Acceleration Driven Clause Learning (Short Paper)
- Termination analysis of programs with multiphase control-flow
- Deciding conditional termination
- Multiphase-linear ranking functions and their relation to recurrent sets
- Deciding conditional termination
This page was built for publication: Proving termination through conditional termination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3303892)
