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

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

1 2 3 ... 5 6 7 next

  1. Beyer, Dirk; Gulwani, Sumit; Schmidt, David A.: Combining model checking and data-flow analysis (2018)
  2. Hensel, Jera; Giesl, Jürgen; Frohn, Florian; Ströder, Thomas: Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution (2018)
  3. Kiefer, Moritz; Klebanov, Vladimir; Ulbrich, Mattias: Relational program reasoning using compiler IR (2018)
  4. Klebanov, Vladimir; Rümmer, Philipp; Ulbrich, Mattias: Automating regression verification of pointer programs by predicate abstraction (2018)
  5. Brockschmidt, Marc; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: Certifying safety and termination proofs for integer transition systems (2017)
  6. Genet, Thomas; Salmon, Yann: Reachability analysis of innermost rewriting (2017)
  7. 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)
  8. Iborra, José; Nishida, Naoki; Vidal, Germán; Yamada, Akihisa: Relative termination via dependency pairs (2017)
  9. Jovanović, Dejan: Solving nonlinear integer arithmetic with MCSAT (2017)
  10. Kop, Cynthia; Middeldorp, Aart; Sternagel, Thomas: Complexity of conditional term rewriting (2017)
  11. Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
  12. McCabe-Dansted, John C.; Reynolds, Mark: Rewrite rules for $\mathrmCTL^\ast$ (2017)
  13. Sabel, David; Zantema, Hans: Termination of cycle rewriting by transformation and matrix interpretation (2017)
  14. Sánchez, Alejandro; Sánchez, César: Parametrized verification diagrams: temporal verification of symmetric parametrized concurrent systems (2017)
  15. Sternagel, Christian; Sternagel, Thomas: Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (2017)
  16. 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)
  17. 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)
  18. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  19. Frohn, Florian; Giesl, Jürgen; Hensel, Jera; Aschermann, Cornelius; Ströder, Thomas: Inferring lower bounds for runtime complexity (2015)
  20. Winkler, Sarah; Thiemann, René: Formalizing soundness and completeness of unravelings (2015)

1 2 3 ... 5 6 7 next


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