Automatically check programs for equivalence


Developed and maintained as part of the IMPROVE project by Mattias Ulbrich, Vladimir Klebanov and Moritz Kiefer.

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

or enter two programs:

Choose a solver

Invariant patterns are hints to the dynamic invariant inference on the terms that could be needed in invariants. These patterns can contain holes represented by _. The dynamic invariant inference instantiates these holes using the variables available in an invariant. It then discards instantiated patterns that do not hold on the analyzed execution traces.

Your programs are sent to the server. Please be a little patient for the answer…

llrêve checks automatically whether two C programs behave equally. For details take a look at the Usage page.