llrêve

Automatically check two 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:

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

        

sat means that the two programs behave equally.
unsat means that there is at least one input on which the programs behave differently. See counterexample below.
If no verdict is presented, the tool may have timed out (TO set to 60s for this server)

SMT2 Code:

        

Counterexample

Counterexample

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