AProVE

AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. AProVE 1.2 is one of the most powerful systems for automated termination proofs of term rewrite systems (TRSs). It is the first tool which automates the new dependency pair framework [8] and therefore permits a completely flexible combination of different termination proof techniques. Due to this framework, AProVE 1.2 is also the first termination prover which can be fully configured by the user.


References in zbMATH (referenced in 148 articles , 1 standard article )

Showing results 101 to 120 of 148.
Sorted by year (citations)
  1. Vidal, Germán: Termination of narrowing in left-linear constructor systems (2008)
  2. Alarcón, Beatriz; Gutiérrez, Raúl; Iborra, José; Lucas, Salvador: Proving termination of context-sensitive rewriting with MU-TERM (2007)
  3. Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador: Improving the context-sensitive dependency graph (2007)
  4. Alarcón, Beatriz; Lucas, Salvador: Termination of innermost context-sensitive rewriting using dependency pairs (2007)
  5. Falke, Stephan; Kapur, Deepak: Dependency pairs for rewriting with non-free constructors (2007)
  6. Fuhs, Carsten; Giesl, Jürgen; Middeldorp, Aart; Schneider-Kamp, Peter; Thiemann, René; Zankl, Harald: SAT solving for termination analysis with polynomial interpretations (2007)
  7. Geser, Alfons; Hofbauer, Dieter; Waldmann, Johannes; Zantema, Hans: On tree automata that certify termination of left-linear term rewriting systems (2007)
  8. Giesl, Jürgen; Kühnemann, Armin; Voigtländer, Janis: Deaccumulation techniques for improving provability (2007)
  9. Hendrix, Joe; Meseguer, José: On the completeness of context-sensitive order-sorted specifications (2007)
  10. Hirokawa, Nao; Middeldorp, Aart: Tyrolean termination tool: techniques and features (2007)
  11. Korp, Martin; Middeldorp, Aart: Proving termination of rewrite systems using bounds (2007)
  12. Kusakari, Keiichirou; Sakai, Masahiko: Enhancing dependency pair method using strong computability in simply-typed term rewriting (2007)
  13. Lucas, Salvador; Navarro-Marset, Rafael: Comparing CSP and SAT solvers for polynomial constraints in termination provers (2007)
  14. Masaki, Nakamura; Kokichi, Futatsugi: On equality predicates in algebraic specification languages (2007)
  15. Payet, Étienne: Detecting non-termination of term rewriting systems using an unfolding operator (2007)
  16. Sereni, Damien: Termination analysis and call graph construction for higher-order functional programs (2007)
  17. Abel, Andreas: Towards generic programming with sized types (2006)
  18. Espada, Miguel Valero; van de Pol, Jaco: Accelerated modal abstractions of labelled transition systems (2006)
  19. Farzan, Azadeh; Meseguer, José: State space reduction of rewrite theories using invisible transitions (2006)
  20. Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René: AProVE 1.2: automatic termination proofs in the dependency pair framework (2006) ioport

Further publications can be found at: http://aprove.informatik.rwth-aachen.de/index.asp?subform=references.html