LARA

This is an old revision of the document!

Symbolic Execution for Example Integer Program

State variables: 

x :: int
y :: int
res :: int

Code: 

res = 0;
i = x;
while (i > 0) {
  i = i - 1;
  res = res + 2;
}