Informace o projektu

Automata for Decision Procedures and Verification (AUTODEV)

Logo poskytovatele
Kód projektu
GA19-24397S
Období řešení
1/2019 - 12/2021
Investor / Programový rámec / typ projektu
Grantová agentura ČR
  • Standardní projekty
Fakulta / Pracoviště MU
Fakulta informatiky
Spolupracující organizace
Vysoké učení technické v Brně
  • Odpovědná osoba Mgr. Lukáš Holík, Ph.D.

Výzkum konečných automatů je tradiční disciplínou, která dlouhodobě produkuje množství výsledků potenciálně využitelných v mnoha oblastech, jako jsou verifikace, zpracování přirozeného jazyka, databáze, nebo webové technologie. Praktická využitelnost těchto výsledků je však limitována nedostatečnou škálovatelností automatové technologie. Protože příčiny této neefektivity tkví v nejzákladnějších technikách a konceptech automatové technologie, potřebný pokrok v této oblasti vyžaduje výrazně nové a přístupy k řešení klasických problémů. V tomto projektu navrhujeme hledat cestu k novým řešením skrze kombinaci tradiční automatové technologie s technikami úspěšnými ve verifikaci a automatickém usuzování, jako jsou líné vyhodnocování, symbolická reprezentace, abstrakce, a techniky SAT/SMT-solvingu. Sílu nových automatových metod pak budeme demonstrovat na několika konkrétních aplikačních doménách: na analýze ukazatelových programů, programů manipulujících řetězce, a na analýze zdrojů a terminace.

Publikace

Počet publikací: 5

2020

2019