Proving Termination of Programs Automatically with AProVE
From MaRDI portal
Publication:3192189
DOI10.1007/978-3-319-08587-6_13zbMath1409.68256OpenAlexW2115215132MaRDI QIDQ3192189
René Thiemann, Florian Frohn, Carsten Otto, Fabian Emmes, Marc Brockschmidt, Peter Schneider-Kamp, Stephanie Swiderski, Carsten Fuhs, Thomas Ströder, Jürgen Giesl, Martin Plücker
Publication date: 26 September 2014
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-08587-6_13
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (22)
Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ Automatically proving termination and memory safety for programs with pointer arithmetic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving ⋮ Automatic discovery of fair paths in infinite-state transition systems ⋮ Termination of Cycle Rewriting by Transformation and Matrix Interpretation ⋮ Satisfiability Checking: Theory and Applications ⋮ Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution ⋮ Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems ⋮ Modular strategic SMT solving with \textbf{SMT-RAT} ⋮ Solving Nonlinear Integer Arithmetic with MCSAT ⋮ Formalizing Soundness and Completeness of Unravelings ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Time-bounded termination analysis for probabilistic programs with delays ⋮ Proving the existence of fair paths in infinite-state systems ⋮ Equational Abstractions in Rewriting Logic and Maude ⋮ Certified abstract cost analysis ⋮ Multi-dimensional interpretations for termination of term rewriting ⋮ Term orderings for non-reachability of (conditional) rewriting ⋮ \textsc{LTL} falsification in infinite-state systems
Uses Software
This page was built for publication: Proving Termination of Programs Automatically with AProVE
