Project Topics in Progress

Pthreads support in Ultimate

Contact: Matthias

1. Develop an extension of Boogie that allows us to model concurrent programs
2. Translate C programs into the (extended Boogie)

Link to project page

Polyhedral Danger Invariants

Contact: Matthias

Transfer idea of 2016FM - David,Kesseli,Kroening,Lewis - Danger Invariants to polyhedral invariants and implement the approach in Ultimate.

Link to project page

Error Localization

Contact: Christian and Matthias

Link to project page
Link to the new webpage

Loop Acceleration

Contact: Daniel or Matthias

We fail to prove that the following program is incorrect, because we have to unroll the loop 10000 times until we find the error.

i := 0;
while (i<10000) {
     i++;
}
assert i==23;

Develop techniques that let us replace the loop by i := 10000 and find the error immediately. See e.g., 2015FMSD - Kroening, Lewis, Weissenbacher - Under-Approximating Loops in C Programs for Fast Counterexample Detection, 2012ISSTA - Strejcek,Trtik - Abstracting Path Conditions, 2010CAV - Bozga,Iosif,Konecny - Fast Acceleration of Ultimately Periodic Relations

Static Heap Separation through Pointer Analysis

Contact: Alexander

The memory model that is currently used by the C-to-Boogie-translation represents C's heap as one large Boogie array (to be precise one per Boogie type). This can cause inefficiency in various places in the verification. We want to apply pointer analysis to be able to split the heap representation into many arrays where we can always be sure which pointer accesses which array.

Data flow graphs for parallel programs

Contact: Alexander

Say we have a way of proving correctness of a program (+ property) given its data flow graph (DFG) which we call data flow proofs.

Given: a parallel program (+ property) P as a set of control flow graphs (one per thread)

Which ways to define the DFG of P are there? What is their effect on the proving power of the data flow proofs?

A trivial way that would retain full proving power is to take the DFG of the interleaving semantics (parallel product) of P (i.e. the CFG that represents all interleavings of the single threads' executions). However the parallel product's size is exponential in the number of threads. Is there a way to avoid this blow-up (at least in some cases)?