CARIBOO
CARIBOO: a multi-strategy termination proof tool based on induction. A termination proof tool for rule-based programs CARIBOO is a termination proof tool for rule-based programming languages, where a program is a rewrite system and query evaluation consists in rewriting a ground expression [3]. It applies to languages such as ASF+SDF, Maude, Cafe-OBJ, or ELAN. By contrast with most of the existing tools, which prove in general termination of standard rewriting (rewriting without strategy) on the free term algebra, our proof tool, named CARIBOO (for Computing AbstRaction for Induction Based termination prOOfs), allows proving termination under specific reduction strategies, which becomes of special interest when the computations diverge for standard rewriting. It deals in particular with: the innermost strategy, specially useful when the rule-based formalism expresses functional programs, and central in the evaluation process of ELAN, local strategies on operators, provided in OBJ-like languages, and allowing to control evaluation strategies in a very fine local way, the outermost strategy, useful to avoid evaluations known to be non terminating for the standard strategy, to make strategy computations shorter, and used for interpreters and compilers using call by name. 2 Proving termination by explicit induction
Keywords for this software
References in zbMATH (referenced in 13 articles )
Showing results 1 to 13 of 13.
Sorted by year (- Meseguer, José: Twenty years of rewriting logic (2012)
- Gnaedig, Isabelle; Kirchner, Hélène: Proving weak properties of rewriting (2011)
- Schernhammer, Felix; Gramlich, Bernhard: Characterizing and proving operational termination of deterministic conditional term rewriting systems (2010)
- Durán, Francisco; Lucas, Salvador; Marché, Claude; Meseguer, José; Urbain, Xavier: Proving operational termination of membership equational programs (2008)
- Borralleras, Cristina; Rubio, Albert: Orderings and constraints: Theory and practice of proving termination (2007)
- Gnaedig, Isabelle; Kirchner, Hélène: Narrowing, abstraction and constraints for proving properties of reduction relations (2007)
- Contejean, Evelyne; Marché, Claude; Tomás, Ana Paula; Urbain, Xavier: Mechanically proving termination using polynomial interpretations (2005)
- Fissore, Olivier; Gnaedig, Isabelle; Kirchner, Hélène: A proof of weak termination providing the right way to terminate (2005)
- Hendrix, Joe; Clavel, Manuel; Meseguer, José: A sufficient completeness reasoning tool for partial specifications (2005)
- Thiemann, René; Giesl, Jürgen: The size-change principle and dependency pairs for termination of term rewriting (2005)
- Fissore, Olivier; Gnaedig, Isabelle; Kirchner, Hélène: Outermost ground termination (2004)
- Kirchner, Claude; Kirchner, Hélène: Rule-based programming and proving: The ELAN experience outcomes (2004)
- Thiemann, René; Giesl, Jürgen; Schneider-Kamp, Peter: Improved modular termination proofs using dependency pairs (2004)