Automatically check programs for equivalence

llrêve

llrêve is an automated program equivalence verification tool. See the project homepage for a description of the approach.

Supported Language

The tool supports most of C99. Bit operations, with the exception of shifts, are not supported.

Marks

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.

Annotations

Either program may be annotated with relational specifications:

/*@ rel_in condition @*/
This clause can be used to define an alternative definition of the input equivalence relation. The clause has to be valid SMT and can contain the function arguments suffixed by $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 @*/
This clause is the correspondant to the above for the output equivalence relation. If this clause is ommitted, equality of both result variables is taken as output relation. An example is included.

Available options

You can specify options using /*@ opt optionname [optval]@*/. Take a look at the example.
Name Description
-dont-instantiateDont instantiate arrays
-fun=<string>Name of the function which should be verified
-heapEnable heap
-infer-marksInfer marks instead of relying on annotations
-init-predIntroduce the toplevel predicate INIT
-inline-letsInline lets
-invertCheck for satisfiabilty of negation
-muzCreate smt intended for conversion to muz
-no-byte-heapTreat each primitive type as a single array entry
-only-recOnly generate recursive invariants
-pass-input-throughPass the input arguments through the complete program. This makes it possible to use them in custom postconditions
-perfect-syncPerfect 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-cfgShow cfg
-show-marked-cfgShow cfg before mark removal
-signedTreat all operations as signed operatons
-stackEnable stack
-stringsSet global constants
-helpDisplay available options (-help-hidden for more)
-help-listDisplay list of available options (-help-list-hidden for more)
-versionDisplay the version of this program

Server performance

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.