Transition Invariants and Transition Predicate Abstraction for Program Termination
From MaRDI portal
Publication:3000631
DOI10.1007/978-3-642-19835-9_2zbMath1315.68104OpenAlexW1496222849MaRDI 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
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Predicate Abstraction for Program Verification, Summarization for termination: No return!, Reverse mathematical bounds for the termination theorem, Convergence: integrating termination and abort-freedom, Automatic synthesis of logical models for order-sorted first-order theories, Liveness Properties in CafeOBJ – A Case Study for Meta-Level Specifications, What's decidable about discrete linear dynamical systems?, Temporal property verification as a program analysis task, The Strength of the SCT Criterion, A Combinatorial Bound for a Restricted Form of the Termination Theorem, Transition Invariants and Transition Predicate Abstraction for Program Termination, Loop Summarization and Termination Analysis, Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems, Automated termination analysis of polynomial probabilistic programs, A DIRECT PROOF OF SCHWICHTENBERG’S BAR RECURSION CLOSURE 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, Explicit Fair Scheduling for Dynamic Control, A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs, Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs, Decision Procedures for Automating Termination Proofs, A complexity tradeoff in ranking-function termination proofs, Proving Termination of Integer Term Rewriting, Temporal prophecy for proving temporal properties of infinite-state systems, Automata-Based Termination Proofs, Automated verification of refinement laws, Mathematics for reasoning about loop functions, Ranking Functions for Linear-Constraint Loops, Termination Analysis of Logic Programs Based on Dependency Graphs, Algebraic model checking for discrete linear dynamical systems
Cites Work
