rêve2 [ Syntax description | Disclaimer ]

Automatically check two programs for equivalence

Developed and maintained as part of the IMPROVE project by Mattias Ulbrich with contributions from Dennis Felsing, Sarah Grebing, Vladimir Klebanov, and Philipp Rümmer.


Load a predefined example:

(examples suffixed with ! contain programs that do not behave equally)

or enter two programs:

Rêve checks automatically whether two C-like programs behave equally. The supported sub-language is restricted. For details see the syntax description.

In particular:

  1. Programs must terminate. Rêve does not check this - it is your responsibility.
  2. Only local variables of type "int" (interpreted as unbounded integers) and "int*" (pointers) are supported.
  3. Local variables must be declared at function beginning.
  4. The return statement must always be the last statement of a function.
  5. Recursive function calls may not occur within the conditions of if or while statements.

You can specify a precondition on the inputs (‣example) and relations that need to hold before and/or after execution (‣example).

Options can be specified in the program files using #pragma instructions (‣example).

For details on the language, assumptions, specifications and options, consult the syntax description.

Your programs are sent to the server. Please be a little patient for the answer... (‣more info)