Objective: The Computer Architecture Lab contributes to the research and development of tools for automated reasoning. This topic stretches from logic, over artificial intelligence to applications and particularly includes support for the development of software and hardware. Our SAT, SMT and QBF solvers are world-renowned and rank at the top of international competitions. Our goal is to bridge the gap between symbolic methods and machine learning, using machine learning to improve symbolic methods and using strong symbolic methods to improve machine learning as well as combining both.

Research Areas: Formal Verification, Hardware Verification, SAT, Theorem Proving