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:

​x
 
1
extern int __mark(int);
2
int f(int t, int c, int r) {
3
  int x = 0;
4
​
5
  if (0 < t) {
6
      while(__mark(42) & (0 < c)) {
7
          x++;
8
          c--;
9
      }
10
  } else {
11
      __mark(23);
12
  }
13
​
14
  while(__mark(13) & (r > 0)) {
15
      x+=2;
16
      r--;
17
  }
18
​
19
  return x;
20
}
21
​
19
 
1
extern int __mark(int);
2
int f(int t, int c, int r) {
3
  int x = 0;
4
​
5
  while(__mark(23) & __mark(42) & (0 < c)) {
6
      if (0 < t) {
7
          x++;
8
      }
9
      c--;
10
  }
11
​
12
  while(__mark(13) & (r > 0)) {
13
      x+=2;
14
      r--;
15
  }
16
​
17
  return x;
18
}
19
​

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.


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

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