Analyzing program termination and complexity automatically with \textsf{AProVE}
From MaRDI portal
Publication:2362493
DOI10.1007/s10817-016-9388-yzbMath1409.68255OpenAlexW2533836568MaRDI QIDQ2362493
Stephanie Swiderski, René Thiemann, Carsten Fuhs, Jürgen Giesl, Jera Hensel, Florian Frohn, Marc Brockschmidt, Fabian Emmes, Carsten Otto, Cornelius Aschermann, Martin Plücker, Thomas Ströder, Peter Schneider-Kamp
Publication date: 10 July 2017
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-016-9388-y
term rewritingcomplexity analysistermination analysisJava programsProlog programsC programsHaskell programs
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (26)
ATLAS: automated amortised complexity analysis of self-adjusting data structures ⋮ Porous invariants ⋮ Loop detection by logically constrained term rewriting ⋮ Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution ⋮ Lower bounds for runtime complexity of term rewriting ⋮ Analyzing Innermost Runtime Complexity Through Tuple Interpretations ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Analysing parallel complexity of term rewriting ⋮ Unnamed Item ⋮ Automated termination analysis of polynomial probabilistic programs ⋮ Proving Termination Through Conditional Termination ⋮ A Perron-Frobenius theorem for deciding matrix growth ⋮ An automated approach to the Collatz conjecture ⋮ Unnamed Item ⋮ From LCF to Isabelle/HOL ⋮ Extended Nested Dual System Groups, Revisited ⋮ Constant runtime complexity of term rewriting is semi-decidable ⋮ Explaining safety failures in NetKAT ⋮ Applications and extensions of context-sensitive rewriting ⋮ Inferring expected runtimes of probabilistic integer programs using expected sizes ⋮ AProVE ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Conditions for confluence of innermost terminating term rewriting systems ⋮ Tuple interpretations for termination of term rewriting ⋮ Type-based analysis of logarithmic amortised complexity ⋮ Runtime complexity analysis of logically constrained rewriting
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Proving termination by dependency pairs and inductive theorem proving
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Compiling finite linear CSP into SAT
- KBO orientability
- Mechanizing and improving dependency pairs
- Matrix interpretations for proving termination of term rewriting
- Isabelle/HOL. A proof assistant for higher-order logic
- Analyzing innermost runtime complexity of term rewriting by dependency pairs
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Lower Runtime Bounds for Integer Programs
- Proving Non-looping Non-termination Automatically
- Dependency Triples for Improving Termination Analysis of Logic Programs with Cut
- Polytool: Polynomial interpretations as a basis for termination analysis of logic programs
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
- Certification of Termination Proofs Using CeTA
- Proving Termination of Programs Automatically with AProVE
- Proving Termination and Memory Safety for Programs with Pointer Arithmetic
- Removing redundant arguments automatically
- Maximal Termination
- Proving Termination by Bounded Increase
- SAT Solving for Termination Analysis with Polynomial Interpretations
- Proving Termination of Integer Term Rewriting
- Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution
- Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs
- Inferring Lower Bounds for Runtime Complexity
- Theory and Applications of Satisfiability Testing
- Ramsey vs. Lexicographic Termination Proving
- Termination Analysis of C Programs Using Compiler Intermediate Languages
- Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting
- Automated Termination Analysis of Java Bytecode by Term Rewriting
- Frontiers of Combining Systems
- Search Techniques for Rational Polynomial Orders
- Computer Aided Verification
- Lazy Abstraction with Interpolants
- Verification, Model Checking, and Abstract Interpretation
This page was built for publication: Analyzing program termination and complexity automatically with \textsf{AProVE}
