10am, November 26th, 2007.
Use latex and email. Prepare a 5-10 min. presentation (demo) of the practical part.
Formalize contraint-based invariant generation for linear arithmetic as presented in class using the introduced terminology, i.e., program transitions, their representation in matrix form, invariant and template maps, etc.
Affine form of Farkas' lemma, as used in the class: if Ax ≤ b has a solution and Ax ≤ b imples cx ≤ δ then there exists a non-negative vector λ such that λ A = c and λ b ≤ δ.
In the class, we used the affine form of Farkas' lemma, which is different from the original lemma. Prove the affine form from the original one (hint: use Duality theorem).
We implement a compiler from CIL expression
language to a string representation in the language
of the clp(q,r) solver. The compiler should only translate the
arithmetic subset, and raise "Not yet implemented" exception on other
inputs. Use single quotes aroung variable names. For example, CIL
representation of the expression x+y <= -z translates to
the string 'x'+'y' =< -'z'.
Extend your C to CFG translator by the compiler for the expression language. Now, the edges of the produced dot-graphs should be decorated by clp(q,r) expressions.
Study the representation of C programs as Prolog terms on the
example in ~rybal/SMC07/symb-exec.pl.
Modify the symbolic execution code to compute the initial condition on states that lead to executions along the select path.
Verify if the computed condition applies to the C programs from which the transition relation is extracted.
Modify the algorithm to enumerate all paths up to the given depth. Verify you modification by using it for finding error paths.
Implement a translator from a subset of C to program representation used in P.2.4.
Test your implementation of symbolic execution on a manually crafted selection of examples containing assertion violations.