Transition invariants and transition predicate abstraction for program termination
From MaRDI portal
Recommendations
- Inductive termination proofs with transition invariants and their relationship to the size-change abstraction
- Transition predicate abstraction and fair termination
- Size-change termination and transition invariants
- Predicate abstraction for program verification
- Loop summarization using state and transition invariants
Cites work
Cited in
(41)- A complexity tradeoff in ranking-function termination proofs
- Automated verification of refinement laws
- Mathematics for reasoning about loop functions
- Convergence: integrating termination and abort-freedom
- Automatic synthesis of logical models for order-sorted first-order theories
- Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
- Temporal prophecy for proving temporal properties of infinite-state systems
- Algebraic model checking for discrete linear dynamical systems
- Automated termination analysis of polynomial probabilistic programs
- Loop summarization using state and transition invariants
- Temporal property verification as a program analysis task
- Execution termination and computation determinacy of data-flow program nets
- Termination criteria for DPO transformations with injective matches
- Liveness properties in CafeOBJ -- a case study for meta-level specifications
- The strength of the SCT criterion
- Transition invariants and transition predicate abstraction for program termination
- Loop Summarization and Termination Analysis
- Decision Procedures for Automating Termination Proofs
- Predicate abstraction for program verification
- Reverse mathematical bounds for the termination theorem
- A combinatorial bound for a restricted form of the termination theorem
- Proving Termination of Integer Term Rewriting
- Automata-Based Termination Proofs
- scientific article; zbMATH DE number 3960981 (Why is no real title available?)
- A direct proof of Schwichtenberg's bar recursion closure theorem
- An intuitionistic version of Ramsey's theorem and its use in program termination
- Parity to safety in polynomial time for pushdown and collapsible pushdown systems
- Explicit fair scheduling for dynamic control
- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs
- Transition predicate abstraction and fair termination
- Ranking functions for linear-constraint loops
- Termination Analysis of Logic Programs Based on Dependency Graphs
- Inductive termination proofs with transition invariants and their relationship to the size-change abstraction
- What's decidable about discrete linear dynamical systems?
- Transition power abstractions for deep counterexample detection
- Commutativity for concurrent program termination proofs
- Invariant relations for affine loops
- On lexicographic proof rules for probabilistic termination
- Inference of ranking functions for proving temporal properties by abstract interpretation
- A new approach for showing termination of parameterized transition systems
- Summarization for termination: No return!
This page was built for publication: Transition invariants and transition predicate abstraction for program termination
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000631)
