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 21 to 40 of 148.
Sorted by year (citations)

previous 1 2 3 4 ... 6 7 8 next

  1. Sabel, David; Zantema, Hans: Termination of cycle rewriting by transformation and matrix interpretation (2017)
  2. Sánchez, Alejandro; Sánchez, César: Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems (2017)
  3. Sternagel, Christian; Sternagel, Thomas: Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (2017)
  4. 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)
  5. Avanzini, Martin; Sternagel, Christian; Thiemann, René: Certification of complexity proofs using CeTA (2015)
  6. Corzilius, Florian; Kremer, Gereon; Junges, Sebastian; Schupp, Stefan; Ábrahám, Erika: \textttSMT-RAT: an open source \textttC++ toolbox for strategic and parallel SMT solving (2015)
  7. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  8. D’Silva, Vijay; Urban, Caterina: Conflict-driven conditional termination (2015)
  9. Frohn, Florian; Giesl, Jürgen; Hensel, Jera; Aschermann, Cornelius; Ströder, Thomas: Inferring lower bounds for runtime complexity (2015)
  10. Winkler, Sarah; Thiemann, René: Formalizing soundness and completeness of unravelings (2015)
  11. Ben-Amram, Amir M.; Genaim, Samir: Ranking functions for linear-constraint loops (2014)
  12. Giesl, Jürgen; Brockschmidt, Marc; Emmes, Fabian; Frohn, Florian; Fuhs, Carsten; Otto, Carsten; Plücker, Martin; Schneider-Kamp, Peter; Ströder, Thomas; Swiderski, Stephanie; Thiemann, René: Proving termination of programs automatically with AProVE (2014)
  13. Kuwahara, Takuya; Terauchi, Tachio; Unno, Hiroshi; Kobayashi, Naoki: Automatic termination verification for higher-order functional programs (2014)
  14. Leuschel, Michael; Vidal, Germán: Fast offline partial evaluation of logic programs (2014)
  15. Roşu, Grigore; Lucanu, Dorel: Behavioral rewrite systems and behavioral productivity (2014)
  16. Schmidt-Schauß, Manfred: Concurrent programming languages and methods for semantic analyses (extended abstract of invited talk) (2014)
  17. Ströder, Thomas; Giesl, Jürgen; Brockschmidt, Marc; Frohn, Florian; Fuhs, Carsten; Hensel, Jera; Schneider-Kamp, Peter: Proving termination and memory safety for programs with pointer arithmetic (2014)
  18. Babić, Domagoj; Cook, Byron; Hu, Alan J.; Rakamarić, Zvonimir: Proving termination of nonlinear command sequences (2013)
  19. Bofill, Miquel; Borralleras, Cristina; Rodríguez-Carbonell, Enric; Rubio, Albert: The recursive path and polynomial ordering for first-order and higher-order terms (2013)
  20. 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) ioport

previous 1 2 3 4 ... 6 7 8 next


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