Developed and maintained as part of the IMPROVE project by Mattias Ulbrich with
contributions from Dennis Felsing,
Load a predefined example:
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
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
For details on the language, assumptions, specifications and options, consult
the syntax description.