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 103 articles , 1 standard article )

Showing results 1 to 20 of 103.
Sorted by year (citations)

1 2 3 4 5 6 next

  1. Brockschmidt, Marc; Joosten, Sebastiaan J.C.; Thiemann, René; Yamada, Akihisa: Certifying safety and termination proofs for integer transition systems (2017)
  2. Giesl, Jürgen; Aschermann, Cornelius; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Analyzing program termination and complexity automatically with \ssfAProVE (2017)
  3. Iborra, José; Nishida, Naoki; Vidal, Germán; Yamada, Akihisa: Relative termination via dependency pairs (2017)
  4. Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
  5. Sternagel, Christian; Sternagel, Thomas: Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (2017)
  6. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter; Aschermann, Cornelius: Automatically proving termination and memory safety for programs with pointer arithmetic (2017)
  7. Corzilius, Florian; Kremer, Gereon; Junges, Sebastian; Schupp, Stefan; Ábrahám, Erika: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving (2015)
  8. Frohn, Florian; Giesl, Jürgen; Hensel, Jera; Aschermann, Cornelius; Ströder, Thomas: Inferring lower bounds for runtime complexity (2015)
  9. Kuwahara, Takuya; Terauchi, Tachio; Unno, Hiroshi; Kobayashi, Naoki: Automatic termination verification for higher-order functional programs (2014)
  10. Leuschel, Michael; Vidal, Germán: Fast offline partial evaluation of logic programs (2014)
  11. Schmidt-Schauß, Manfred: Concurrent programming languages and methods for semantic analyses (extended abstract of invited talk) (2014)
  12. Babić, Domagoj; Cook, Byron; Hu, Alan J.; Rakamarić, Zvonimir: Proving termination of nonlinear command sequences (2013)
  13. Bofill, Miquel; Borralleras, Cristina; Rodríguez-Carbonell, Enric; Rubio, Albert: The recursive path and polynomial ordering for first-order and higher-order terms (2013)
  14. Giesl, Jürgen; Ströder, Thomas; Schneider-Kamp, Peter; Emmes, Fabian; Fuhs, Carsten: Symbolic evaluation graphs and term rewriting -- a general methodology for analyzing logic programs. (Abstract) (2013)
  15. Winkler, Sarah; Sato, Haruhiko; Middeldorp, Aart; Kurihara, Masahito: Multi-completion with termination tools (2013)
  16. Borralleras, Cristina; Lucas, Salvador; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: SAT modulo linear arithmetic for solving polynomial constraints (2012)
  17. Bouhoula, Adel; Jacquemard, Florent: Sufficient completeness verification for conditional and constrained TRS (2012)
  18. Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René: SAT solving for termination proofs with recursive path orders and dependency pairs (2012)
  19. Meseguer, José: Twenty years of rewriting logic (2012)
  20. Brockschmidt, Marc; Otto, Carsten; Giesl, Jürgen: Modular termination proofs of recursive Java bytecode programs by term rewriting (2011)

1 2 3 4 5 6 next


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