Mgr. Mikoláš Janota, Ph.D.

Satisfiability modulo theories (SMT) aim at providing push-button technology for solving hard problems coming from practice and that can be formalized in mathematical logic. The sources of applications are for example software testing or verification. However, modern SMT solvers do not learn any new information from solving one problem that could be carried to another problem. In contrast, modern machine learning (ML) techniques enable improving algorithms over time. The topic of this thesis is to build on top of existing SMT algorithms and extend them with ML techniques to qualitatively improve state-of-the-art solvers.