|Project name:||POSTMAN – Powering SMT Solvers by Machine Learning|
|Supported by:||Ministry of Education, Youth and Sports (MEYS / MŠMT)|
|Budget:||38 916 mil. CZK|
|Project duration:||01/2020 – 12/2024|
|Main investigator:||Mgr. Mikoláš Janota, Ph.D.|
The POSTMAN project aims 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.
POSTMAN will very significantly advance SMT solving by developing Machine Learning methods that prune the search space of the solvers. Unlike the current search methods, Machine Learning allows to take into account a large number of observations made during the proof searches, and recommend the most relevant course of action.
The project will develop learning based guiding methods at various levels of abstraction, focusing on two critical problems in SMT and its applications: solving of quantified formulas and solving of classes of formulas.
The expected outcome of the project is a range of new powerful methods combining Machine Learning techniques with current logic-based SMT approaches, providing significant improvement over current state of the art. The methods will be integrated in a number of systems and deployed in major SMT applications, benefiting large parts of today’s formal verification.
“Results of this project No. LL1902 were supported by the Ministry of Education, Youth and Sports within the programme ERC CZ“