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íce informací na neformální webové stránce skupiny.