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 41 to 60 of 148.
Sorted by year (citations)
  1. Winkler, Sarah; Sato, Haruhiko; Middeldorp, Aart; Kurihara, Masahito: Multi-completion with termination tools (2013)
  2. Ben-Amram, Amir M.; Genaim, Samir; Masud, Abu Naser: On the termination of integer loops (2012)
  3. Borralleras, Cristina; Lucas, Salvador; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: SAT modulo linear arithmetic for solving polynomial constraints (2012)
  4. Bouhoula, Adel; Jacquemard, Florent: Sufficient completeness verification for conditional and constrained TRS (2012)
  5. Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René: SAT solving for termination proofs with recursive path orders and dependency pairs (2012)
  6. Meseguer, José: Twenty years of rewriting logic (2012)
  7. Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador; Navarro-Marset, Rafael: Proving termination properties with \textscmu-term (2011)
  8. Brockschmidt, Marc; Otto, Carsten; Giesl, Jürgen: Modular termination proofs of recursive Java bytecode programs by term rewriting (2011)
  9. Durand, Irène; Sylvestre, Marc: Left-linear bounded TRSs are inverse recognizability preserving (2011)
  10. Endrullis, Jörg; Hendriks, Dimitri: Lazy productivity via termination (2011)
  11. Fuhs, Carsten; Giesl, Jürgen; Parting, Michael; Schneider-Kamp, Peter; Swiderski, Stephan: Proving termination by dependency pairs and inductive theorem proving (2011)
  12. Fuhs, Carsten; Kop, Cynthia: Harnessing first order termination provers using higher order dependency pairs (2011)
  13. Krauss, Alexander; Sternagel, Christian; Thiemann, René; Fuhs, Carsten; Giesl, Jürgen: Termination of Isabelle functions via termination of rewriting (2011)
  14. Sakata, Tsubasa; Nishida, Naoki; Sakabe, Toshiki: On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs (2011)
  15. Sternagel, Christian; Thiemann, René: Generalized and formalized uncurrying (2011)
  16. Stump, Aaron; Kimmell, Garrin; El Haj Omar, Roba: Type preservation as a confluence problem (2011)
  17. Voets, Dean; De Schreye, Danny: Non-termination analysis of logic programs with integer arithmetics (2011)
  18. Winkler, Sarah; Middeldorp, Aart: AC completion with termination tools (2011)
  19. Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador: Context-sensitive dependency pairs (2010)
  20. Alpuente, M.; Escobar, S.; Gramlich, B.; Lucas, S.: On-demand strategy annotations revisited: an improved on-demand evaluation strategy (2010)

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