Formal Verification Group

About us

We are interested in formal methods for the correct construction of hardware and soft­ware systems. Our focus is on automated methods for checking compliance of an implementation with a specification, and in particular Model Checking.

We are particularily interested in applying these methods to practical hardware and software im­ple­mentations given in industrial languages such as Verilog, C or C++. Read more about software verif­ication or hardware verification.

NEW: We are hiring Postdocs and PhD students!

Recent Publications

• New: Interpolant Strength
• New: Automatic Analysis of Scratch-pad Memory Code for Heterogeneous Multicore Processors
• New: Ranking Function Synthesis for Bit-Vector Relations
• New: Boom: Analyzing Boolean Programs with Unbounded Concurrency
• Symbolic Counter Abstraction for Concurrent Software
• Race Analysis for SystemC using Model Checking
• Deciding Bit-Vector Arithmetic with Abstraction
• Counterexamples with Loops for Predicate Abstraction

Funding