CARIBOO is a prototype implementing an original induction-based approach for proving properties of rewriting under strategies.

CARIBOO (for Computing AbstRaction for Induction Based termination prOOfs), is currently dedicated to termination proofs 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 their evaluation process,
• local strategies on operators, provided in OBJ-like languages, and allowing to control evaluation strategies in a very precise 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.

This prototype 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. It applies to languages such as ASF+SDF, Maude, Cafe-OBJ, or ELAN.

The proof technique of CARIBOO relies on a generic inductive process, instantiated for the different considered strategies. It generates ordering and abstraction constraints automatically solved, or delegated to an external constraint solver, or let to the user.