Proving termination of programs automatically with AProVE
From MaRDI portal
Publication:3192189
DOI10.1007/978-3-319-08587-6_13zbMATH Open1409.68256OpenAlexW2115215132MaRDI QIDQ3192189FDOQ3192189
Authors: Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Stephanie Swiderski, René Thiemann 
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 (37)
- 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
- Term orderings for non-reachability of (conditional) rewriting
- Decision Procedures for Automating Termination Proofs
- Equational abstractions in rewriting logic and Maude
- Automata-Based Termination Proofs
- Complexity of conditional term rewriting
- Title not available (Why is that?)
- Formalizing soundness and completeness of unravelings
- Solving nonlinear integer arithmetic with MCSAT
- Termination of cycle rewriting by transformation and matrix interpretation
- Termination graphs for Java bytecode
- Modular termination proofs of recursive Java bytecode programs by term rewriting
- Proof Pearl: The Termination Analysis of Terminator
- Tools and Algorithms for the Construction and Analysis of Systems
- Reachability analysis of innermost rewriting
- Proving termination of programs with bitvector arithmetic by symbolic execution
- A context-based approach to proving termination of evaluation
- Title not available (Why is that?)
- Certified abstract cost analysis
- Proving the existence of fair paths in infinite-state systems
- Satisfiability checking: theory and applications
- Automated termination analysis of Java bytecode by term rewriting
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Complexity analysis for \textbf{Java} with \textsf{AProVE}
- 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
- Termination Competition (termCOMP 2015)
- Automata-based termination proofs
- Kruskal's tree theorem for acyclic term graphs
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- 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)
