Obohacování SMT řešičů pomocí strojového učení

Poskytovatel

Ministerstvo školství, mládeže a tělovýchovy

Program

ERC CZ

Veřejná soutěž

SMSM2019LL001

Hlavní účastníci

České vysoké učení technické v Praze / Český institut informatiky, robotiky a kybernetiky

Druh soutěže

VS - Veřejná soutěž

Číslo smlouvy

MSMT-35696/2019-1

Název projektu anglicky

Powering SMT Solvers by Machine Learning

Anotace anglicky

"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."

Kategorie VaV

ZV - Základní výzkum

OECD FORD - hlavní obor

20202 - Communication engineering and systems

OECD FORD - vedlejší obor

—

OECD FORD - další vedlejší obor

—

CEP - odpovídající obory <br>(dle <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">převodníku</a>)

JW - Navigace, spojení, detekce a protiopatření

Zahájení řešení

1. 1. 2020

Ukončení řešení

31. 12. 2025

Poslední stav řešení

B - Běžící víceletý projekt

Poslední uvolnění podpory

10. 1. 2024

Důvěrnost údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Systémové označení dodávky dat

CEP24-MSM-LL-R

Datum dodání záznamu

19. 2. 2024

Celkové uznané náklady

38 916 tis. Kč

Výše podpory ze státního rozpočtu

38 916 tis. Kč

Ostatní veřejné zdroje financování

0 tis. Kč

Neveřejné tuz. a zahr. zdroje finan.

0 tis. Kč