Proving termination of programs automatically with AProVE
From MaRDI portal
Publication:3192189
DOI10.1007/978-3-319-08587-6_13zbMATH Open1409.68256OpenAlexW2115215132MaRDI QIDQ3192189FDOQ3192189
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
Recommendations
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Automated termination proofs for logic programs by term rewriting
- Complexity analysis for \textbf{Java} with \textsf{AProVE}
- Automated termination analysis of Java bytecode by term rewriting
- Modular termination proofs of recursive Java bytecode programs by term rewriting
Cited In (30)
- Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- \textsc{LTL} falsification in infinite-state systems
- Time-bounded termination analysis for probabilistic programs with delays
- Multi-dimensional interpretations for termination of term rewriting
- Automatic discovery of fair paths in infinite-state transition systems
- Logic for Programming, Artificial Intelligence, and Reasoning
- Satisfiability Checking: Theory and Applications
- Title not available (Why is that?)
- Term orderings for non-reachability of (conditional) rewriting
- Decision Procedures for Automating Termination Proofs
- Automata-Based Termination Proofs
- SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
- Title not available (Why is that?)
- Equational Abstractions in Rewriting Logic and Maude
- Proof Pearl: The Termination Analysis of Terminator
- A context-based approach to proving termination of evaluation
- Title not available (Why is that?)
- Title not available (Why is that?)
- Certified abstract cost analysis
- Solving Nonlinear Integer Arithmetic with MCSAT
- Formalizing Soundness and Completeness of Unravelings
- Proving the existence of fair paths in infinite-state systems
- Termination of Cycle Rewriting by Transformation and Matrix Interpretation
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
- Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
- Title not available (Why is that?)
- Modular strategic SMT solving with \textbf{SMT-RAT}
- Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
Uses Software
This page was built for publication: Proving termination of programs automatically with AProVE
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192189)
