Detail projektu

ROULETTE - Reprezentace Booleovských funkcí pomocí adaptabilní datové struktury

Období řešení: 1. 1. 2023 - 31. 12. 2025

Typ projektu: grant

Kód: GA23-07565S

Agentura: Grantová agentura České republiky

Program: Standardní projekty

Název anglicky
Representing Boolean Functions by a Self-Adaptable Data Structure
Typ
grant
Klíčová slova

logiky;modely;binární rozhodovací diagramy;BDD;automaty;kompaktnost;efektivita;formální modely;formální verifikace

Abstrakt

Lidstvo čím dál více závisí na počítačových systémech, což klade vysoké nároky na jejich bezchybnost a efektivitu. Tyto systémy jsou stále složitější: jejich stavové prostory rostou exponenciálně a současné techniky pro zajištění bezchybnosti neškálují. Chyby se dostávají do reálného nasazení, což způsobuje finanční a lidské ztráty. Tento projekt se zaměřuje na výzkum nových metod pro kompaktní reprezentaci obrovských stavových prostorů těchto systémů. Této kompaktni reprezentace dosáhnu spojením bohaté, ale těžko proniknutelné, teorie automatů a oblastí solverů a formální verifikace, které se zaměřují na výkon v reálných aplikacích. Dané spojení povede k vytvoření nové flexibilní a adaptabilní datové struktury schopné využít vnitřní struktury systémů k jejich kompaktní reprezentaci. Nad datovou strukturou pak vyvinu nástroje schopné manipulovat se stavovými prostory dosud nevídané velikosti. Toto nové paradigma od základů změní pohled na reprezentaci stavových prostorů a bude moci sloužit jako základní technologie pro tvorbu rychlých, bezchybných a bezpečných systémů pro budoucnost.

Řešitelé
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT) , hlavní řešitel
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT)
Havlena Vojtěch, Ing., Ph.D. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Publikace

2023

Nahoru