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:

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.

The CARIBOO home page