Powering SMT Solvers by Machine Learning
Public support
Provider
Ministry of Education, Youth and Sports
Programme
ERC CZ
Call for proposals
SMSM2019LL001
Main participants
České vysoké učení technické v Praze / Český institut informatiky, robotiky a kybernetiky
Contest type
VS - Public tender
Contract ID
MSMT-35696/2019-1
Alternative language
Project name in Czech
Obohacování SMT řešičů pomocí strojového učení
Annotation in Czech
"Cílem projektu POSTMAN je dosáhnout průlomu v oblasti Splnitelnost Modulo Teorie (SMT) pomocí vývoje metod strojového učení cílených na kritické části dnešních procedur pro řešení SMT. Řešiče SMT jsou účinné nástroje, které uvažují nad fragmenty logiky prvního řádu se zaměřením na praktické aplikace. Tyto nástroje hrají stěžejní roli v ověřování a testování softwaru, hardwaru a příbuzných oblastech. K řešení problémů z reálného světa, mnoho nástrojů závisí na SMT tím, že překládají daný problém do formulace matematické logiky a delegují jeho řešení SMT řešiči. SMT se tímto ocitá v jádru dnešních verifikačních nástrojů, které se systematicky spouští na tisících procesorech ve velkých softwarových a hardwarových firmách. SMT systémy usilují o poskytnutí plné automatizace, ale oproti tomu musí řešit ze své podstaty těžké problémy. Pokud nástroj nevyřeší daný problém v požadovaném čase, uživatelé jsou nuceni reformulovat tento problém nebo poskytnout řešiči nápovědu. Oba scénáře jsou nežádoucí tím že vyžadují další úsilí a značnou znalost používaného nástroje. POSTMAN velmi výrazně pokročí v řešení SMT rozvíjením metod strojového učení, které prořezávají prohledávací prostor problému. Na rozdíl od současných metod prohledávání, strojové učení umožňuje brát v úvahu velký počet pozorování provedených během hledání důkazů a doporučit nejrelevantnější postup. Projekt bude rozvíjet učící metody na různých úrovních abstrakce se zaměřením na dva kritické problémy v SMT a jeho aplikacích: řešení kvantifikovaných formulí a řešení tříd formulí. Očekávaným výstupem projektu je řada nových výkonných metod kombinujících techniky strojového učení se současnými přístupy SMT založenými na logice, které poskytnou výrazné zlepšení oproti současnému stavu. Tyto metody budou integrovány do řady systémů a nasazeny ve významných SMT aplikacích, používaných ve velké části moderního formálního ověřování."
Scientific branches
R&D category
ZV - Basic research
OECD FORD - main branch
20202 - Communication engineering and systems
OECD FORD - secondary branch
—
OECD FORD - another secondary branch
—
CEP - equivalent branches <br>(according to the <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">converter</a>)
JW - Navigation, connection, detection and countermeasure
Solution timeline
Realization period - beginning
Jan 1, 2020
Realization period - end
Dec 31, 2025
Project status
B - Running multi-year project
Latest support payment
Jan 10, 2024
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP24-MSM-LL-R
Data delivery date
Feb 19, 2024
Finance
Total approved costs
38,916 thou. CZK
Public financial support
38,916 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK