Formal Methods Group

at the AI Department of CIIRC at CTU in Prague

Our goal

We aim at a breakthrough in the field of Satisfiability Modulo Theories (SMT) by developing Machine Learning methods targeted at the critical parts of today’s SMT procedures.

SMT solvers are efficient tools that reason about fragments of first order logic with focus on practical applications. These tools play a crucial role in verification and testing of software, hardware and related areas. To solve real-world problems, many tools rely on SMT by translating the problems into a logic formulation and delegating their solution to the SMT solvers. SMT is thus at the heart of today’s large verification toolchains, run continuously on thousands of CPUs by major software and hardware companies around the world. SMT systems strive to provide push-button technology, however, they need to handle inherently hard problems. Failing to solve a problem in reasonable time means that the users are forced to reformulate the problem or to provide the solver with hints. Both scenarios are undesirable, requiring extra effort and considerable SMT expertise.

Research topics