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
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 @*/
$2_0depending 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.
|-dont-instantiate||Dont instantiate arrays|
|-fun=<string>||Name of the function which should be verified|
|-infer-marks||Infer marks instead of relying on annotations|
|-init-pred||Introduce the toplevel predicate INIT|
|-invert||Check for satisfiabilty of negation|
|-muz||Create smt intended for conversion to muz|
|-no-byte-heap||Treat each primitive type as a single array entry|
|-only-rec||Only generate recursive invariants|
|-pass-input-through||Pass the input arguments through the complete program. This makes it possible to use them in custom postconditions|
|-perfect-sync||Perfect synchronization, don’t allow off by n loops|
|-resource-dir=<string>||Directory containing the clang resource files, e.g. /usr/local/lib/clang/3.8.0|
|-show-marked-cfg||Show cfg before mark removal|
|-signed||Treat all operations as signed operatons|
|-strings||Set global constants|
|-help||Display available options (-help-hidden for more)|
|-help-list||Display list of available options (-help-list-hidden for more)|
|-version||Display the version of this program|
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.