llrêve is an automated program equivalence verification tool. See the project homepage for a description of the approach.
The tool supports most of C99. Bit operations, with the exception of shifts, are not supported.
llrêve requires you to annotate your program with marks which
represent synchronization points between the two programs. In
most cases those synchronization points can simply be the loop
header. You need to first declare the mark function
using extern int __mark(int); and then place it
at the points that you synchronize using the same number as
argument in both programs. You can also associate multiple marks with the same point, take look at the example for
the details on that.
Either program may be annotated with relational specifications:
/*@ rel_in condition @*/$1_0 or $2_0 depending
on which program they refer to. If this clause is ommitted, equality
of all parameters is taken as input relation. An example is
included.
/*@ rel_out condition @*//*@ opt optionname [optval]@*/.
Take a look at the example.
| Name | Description |
|---|
This service is currently run on a stock virtualized server that shares its underlying hardware with other services. It is therefore that the performance of rêve is unpredictable and may deviate from run to run. Moreover, each time you launch a query to the server a Java Virtual Machine (JVM) needs to be launched. For the experiments in the papers, we used the SMT solver Eldarica in a client-server-mode avoiding the JVM startup time. This is not possible on the server for technical reasons. The runtimes you experience may hence be considerably longer than in the paper.