Proving termination of programs automatically with AProVE
From MaRDI portal
(Redirected from 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
(39)- Analyzing program termination and complexity automatically with \textsf{AProVE}
- \textsc{LTL} falsification in infinite-state systems
- Multi-dimensional interpretations for termination of term rewriting
- Time-bounded termination analysis for probabilistic programs with delays
- 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
- Formalizing soundness and completeness of unravelings
- Solving nonlinear integer arithmetic with MCSAT
- scientific article; zbMATH DE number 970706 (Why is no real title available?)
- 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
- Reachability analysis of innermost rewriting
- Tools and Algorithms for the Construction and Analysis of Systems
- A context-based approach to proving termination of evaluation
- Proving termination of programs with bitvector arithmetic by symbolic execution
- Termination of graph transformation systems via generalized weighted type graphs
- Certified abstract cost analysis
- scientific article; zbMATH DE number 7453196 (Why is no real title available?)
- Proving the existence of fair paths in infinite-state systems
- Checking linear integer arithmetic proofs in Lambdapi
- 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}
- 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
- 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
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)
