FM: Formální metody

Náš cíl: Snažíme se dosáhnout průlomu v oblasti Splnitelnost Modulo Teorie (SMT) pomocí vývoje metod strojového učení zaměřených na kritické části dnešních postupů SMT. SMT řešiče jsou efektivní nástroje, které uvažují o fragmentech logiky prvního řádu s důrazem na praktické aplikace.

Tyto nástroje hrají klíčovou roli při ověřování a testování softwaru, hardwaru a příbuzných oblastí. Pro řešení problémů reálného světa mnoho nástrojů spoléhá na SMT tím, že převedou problémy do logické formulace a delegují jejich řešení SMT řešičům. SMT je tak v jádru dnešních rozsáhlých řetězců nástrojů pro ověřování, které jsou nepřetržitě spouštěny na tisících CPU velkými softwarovými a hardwarovými firmami po celém světě. SMT systémy se snaží poskytovat technologie na jeden stisk tlačítka, ale musí se vypořádat s inherentně obtížnými problémy. Neschopnost vyřešit problém v rozumném čase znamená, že uživatelé jsou nuceni přeformulovat problém nebo poskytnout řešiči nápovědu. Oba scénáře jsou nežádoucí a vyžadují dodatečné úsilí a značnou odbornost v oblasti SMT.

Témata výzkumu:

• Strojové učení

• Splnitelnost Modulo Teorie (SMT)

• Problém Splnitelnosti (SAT Solving)

Projekt: Postman

Vědečtí pracovníci: Chad E. Brown, Jan Jakubův, Karel Chvalovský, Jan Hůla

Doktorandi: Nikolai Antonov

Více informací na neformální webové stránce skupiny.

Vedoucí skupiny

Mikoláš Janota
Email: mikolas.janota(at)cvut.cz