Informace o projektu

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.