Proving termination of programs automatically with AProVE
From MaRDI portal
Publication:3192189
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)- Modular termination proofs of recursive Java bytecode programs by term rewriting
- Complexity of conditional term rewriting
- Automata-based termination proofs
- Certified abstract cost analysis
- Automatic discovery of fair paths in infinite-state transition systems
- Term orderings for non-reachability of (conditional) rewriting
- Satisfiability checking: theory and applications
- Automated termination analysis of Java bytecode by term rewriting
- \texttt{SMT-RAT}: an open source \texttt{C++} toolbox for strategic and parallel SMT solving
- Proving termination of programs with bitvector arithmetic by symbolic execution
- Automatically proving termination and memory safety for programs with pointer arithmetic
- Proof Pearl: The Termination Analysis of Terminator
- A context-based approach to proving termination of evaluation
- Automata-Based Termination Proofs
- scientific article; zbMATH DE number 970706 (Why is no real title available?)
- Termination Competition (termCOMP 2015)
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
- Tools and Algorithms for the Construction and Analysis of Systems
- Termination of cycle rewriting by transformation and matrix interpretation
- Kruskal's tree theorem for acyclic term graphs
- Equational abstractions in rewriting logic and Maude
- \textsc{LTL} falsification in infinite-state systems
- Proving the existence of fair paths in infinite-state systems
- Reachability analysis of innermost rewriting
- Modular strategic SMT solving with \textbf{SMT-RAT}
- Time-bounded termination analysis for probabilistic programs with delays
- Termination graphs for Java bytecode
- scientific article; zbMATH DE number 7453196 (Why is no real title available?)
- Logic for Programming, Artificial Intelligence, and Reasoning
- Formalizing soundness and completeness of unravelings
- Decision Procedures for Automating Termination Proofs
- Solving nonlinear integer arithmetic with MCSAT
- Multi-dimensional interpretations for termination of term rewriting
- Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems
- Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
- Complexity analysis for \textbf{Java} with \textsf{AProVE}
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)
