This page lists some of our projects in formal verification on all levels, e.g. Bachelor, Master and PhD projects. Most of them have a theoretical background but also more often than not require good low-level implementation skills.
The AIGER format can be used to capture simple model checking benchmarks. Only simple safety properties and fair cycle detection is supported at the moment. The project is about handling PSL.
In the context of the Ph.D. thesis of Cyrille Artho we implemented JNuke, a model checker framework for Java. We are looking for an interested student to add an application layer on top of the framework in order to be able to formally release the code. There is also another paper describing the test process we used for JNuke.
Satisfiabiliy checking (SAT) is a fast moving technology and is used in many applications, from hardware verification to device driver verification. We developed C32SAT which generates SAT instances from C expressions (Robert Brummayer). We want to extend the subset of the C language that our tool can handle.
Another topic is to use specialized hardware, such as graphics processing units, for faster SAT algorithms.
But we also continue to work on core engines: restart policies, structural solvers, preprocessing, etc.
In the past we have been working on binary decision diagrams (BDDs) which in recent years became a rather neglected research subject. Still there are open issues such as efficient 64-bit support, more advanced garbage collection and resource limited operations.
Satisfiability modulo theories (SMT) is the generic term to describe decision procedures for certain logics without quantifiers. Examples for such theories are integers, reals, uninterpreted functions and arrays, having mostly applications in software verification. In one project we are working on a specific approach that uses SAT solver technology. In another project we work on specific semantics of arithmetic operations given by programming languages such as Verilog and C.
We are interested in synthesizing hardware models for verification purposes. A challenging compiler project is to generate flat cycle accurate circuits from Verilog models.
Decision procedures for Quantified Boolean Formulas (QBF) can be used to handle various verification problems. Recently these procedures became much more powerful, though benchmarking in the real world and adapting QBF solvers to real problem domains has not been investigated much. In another project we want to work on new solver technology.