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

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

1 2 3 ... 6 7 8 next

  1. Caltais, Georgiana; Tunç, Hünkar Can: Explaining safety failures in NetKAT (2021)
  2. Lucas, Salvador: Using well-founded relations for proving operational termination (2020)
  3. Lucas, Salvador; Meseguer, José; Gutiérrez, Raúl: The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques (2020)
  4. van Doorn, Floris; Ebner, Gabriel; Lewis, Robert Y.: Maintaining a library of formal mathematics (2020)
  5. Xu, Ming; Deng, Yuxin: Time-bounded termination analysis for probabilistic programs with delays (2020)
  6. Albert, Elvira; Bofill, Miquel; Borralleras, Cristina; Martin-Martin, Enrique; Rubio, Albert: Resource analysis driven by (conditional) termination proofs (2019)
  7. Fuhs, Carsten: Transforming derivational complexity of term rewriting to runtime complexity (2019)
  8. Ishizuki, Sayaka; Oyamaguchi, Michio; Sakai, Masahiko: Conditions for confluence of innermost terminating term rewriting systems (2019)
  9. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  10. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  11. Frohn, Florian; Giesl, Jürgen: Constant runtime complexity of term rewriting is semi-decidable (2018)
  12. Hensel, Jera; Giesl, Jürgen; Frohn, Florian; Ströder, Thomas: Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution (2018)
  13. Kiefer, Moritz; Klebanov, Vladimir; Ulbrich, Mattias: Relational program reasoning using compiler IR (2018)
  14. Klebanov, Vladimir; Rümmer, Philipp; Ulbrich, Mattias: Automating regression verification of pointer programs by predicate abstraction (2018)
  15. Kremer, Gereon; Ábrahám, Erika: Modular strategic SMT solving with \textbfSMT-RAT (2018)
  16. Brockschmidt, Marc; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: Certifying safety and termination proofs for integer transition systems (2017)
  17. Frohn, Florian; Giesl, Jürgen; Hensel, Jera; Aschermann, Cornelius; Ströder, Thomas: Lower bounds for runtime complexity of term rewriting (2017)
  18. Fuhs, Carsten; Kop, Cynthia; Nishida, Naoki: Verifying procedural programs via constrained rewriting induction (2017)
  19. Genet, Thomas; Salmon, Yann: Reachability analysis of innermost rewriting (2017)
  20. 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 \textsfAProVE (2017)

1 2 3 ... 6 7 8 next


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