Project Topics in Progress

Dynamic POR for Verification of Concurrent Programs with Loops

Contact: Dominik

Link to project page

Counting-Automata

Contact: Matthias

Link to project page

Constraint-based Invariant Synthesis

Contact: Matthias

Link to project page

From Pthreads to Petri Nets

Contact: Matthias

Link to project page

Partial Quantifier Elimination for the Theory of Arrays

Contact: Matthias

Link to project page

PredicateTrie-based Predicate Unifier

Contact: Daniel

Description follows.

Implement "Property driven reachability"

Contact: Daniel

• Interpolating Property Directed Reachability
• Efficient implementation of property directed reachability
• IC3 - Flipping the E in ICE

Description follows.

Array Content Analysis for Abstract Interpretation

Contact: Daniel

• POPL11. Cousot, Cousot, Logozzo. A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis.

Bitvector to Integer translation

Translate a bitvector representation of a program into an integer representation of a program. Contact: Matthias

Link to project page

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

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)?