Automatically check programs for equivalence

llrêve

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

Which solver should I choose?

llrêve reduces the problem of checking the programs for equivalence to a set of SMT clauses. These clauses are then passed to an SMT solver. You can select two different SMT solvers in the webinterface, namely Z3 and Eldarica. You can choose between two separate inference engines built into Z3 (called duality and spacer). In addition to that you can also choose Dynamic invariant inference. In this case llrêve tries to infer invariants by executing the two programs and analyzing these execution traces. The task of checking whether these invariants hold and whether they are strong enough to prove equivalence is delegated to Z3. Finally you can also choose the Race-option. In this case Z3, Eldarica and the dynamic invariant inference are started in parallel and the result of the fastest procedure is returned.



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.

How do I specify invariant patterns?

Each line represents one pattern and needs to be terminated by ;.

Available operators

/\ boolean conjunction
\/ boolean disjunction
+,-,* addition, subtraction, multiplication
_ Hole that will be instantiated using available variables
<,<=,=,>=,> integer comparisons

Your programs are sent to the server. Please be a little patient for the answer…
Checking
Running llrêve
Running solver
Verdict
Invariants
SMT2 Code
Counterexample Counterexample
LLVM IR

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