Transition Invariants and Transition Predicate Abstraction for Program Termination

DOI10.1007/978-3-642-19835-9_2zbMath1315.68104MaRDI QIDQ3000631

Andreas Podelski, Andrey Rybalchenko

Publication date: 19 May 2011

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

Full work available at URL: https://doi.org/10.1007/978-3-642-19835-9_2

Mathematics Subject Classification ID

68Q60: Specification and verification (program logics, model checking, etc.)

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

Related Items

A DIRECT PROOF OF SCHWICHTENBERG’S BAR RECURSION CLOSURE THEOREM, 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, Ranking Functions for Linear-Constraint Loops, Termination Analysis of Logic Programs Based on Dependency Graphs, What's decidable about discrete linear dynamical systems?, Reverse mathematical bounds for the termination theorem, An intuitionistic version of Ramsey's theorem and its use in program termination, Inference of ranking functions for proving temporal properties by abstract interpretation, Summarization for termination: No return!, 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, Temporal property verification as a program analysis task, 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, A Combinatorial Bound for a Restricted Form of the Termination Theorem, Proving Termination of Integer Term Rewriting, Automata-Based Termination Proofs

Cites Work