The main objective is making automated reasoning techniques and tools applicable to a wider range of problems, as well as making them easier to use by researchers, software developers, hardware designers, and information system users and developers. The Action coordinates activities on developing infrastructures for automated reasoning about the new notion of Rich Models of computer systems. Rich Models have the expressive power of a large fragment of formalizable mathematics, enabling specification of software, hardware, embedded, and distributed systems. Rich Models support modeling at a wide range of abstraction levels, from knowledge bases and system architecture, to software source code and detailed hardware design. The Action contributes to the construction of Rich-Model Toolkit, a new unified infrastructure that precisely defines the meaning of Rich Models, introduces standardized representation formats, and incorporates a number of automated reasoning tools. Moreover, the Action develops and deploys new tools for automated reasoning that communicate using these standardized formats. The resulting tools will have a wide range of applicability and improved efficiency, helping system developers construct reliable systems through automated reasoning, analysis, and synthesis.

Popis česky
Projekt se zaměřuje na vývoj bohatého modelovacího jazyka a s ním spojené infrastruktury pro formální verifikaci a syntézu, přispívající k vývoji spolehlivých počítačových systémů.

Klíčová slova
formal modelling, formal verification, decision procedures, synthesis

IC0901

angličtina

Kuncak Viktor - hlavní řešitel
Češka Milan, prof. RNDr., CSc. - spoluřešitel
Dudka Kamil, Ing. - spoluřešitel
Fiedor Jan, Ing., Ph.D. - spoluřešitel
Gach Marek, Ing. - spoluřešitel
Holík Lukáš, doc. Mgr., Ph.D. - spoluřešitel
Hýsek Jiří, Ing. - spoluřešitel
Konečný Filip, Ing., Ph.D. - spoluřešitel
Křena Bohuslav, Ing., Ph.D. - spoluřešitel
Letko Zdeněk, Ing., Ph.D. - spoluřešitel
Peringer Petr, Dr. Ing. - spoluřešitel
Rogalewicz Adam, doc. Mgr., Ph.D. - spoluřešitel
Smrčka Aleš, Ing., Ph.D. - spoluřešitel
Šimáček Jiří, Ing., Ph.D. - spoluřešitel

Ústav inteligentních systémů
- odpovědné pracoviště (28.11.2009 - nezadáno)
Výzkum informačních technologií z hlediska bezpečnosti
- interní (30.10.2009 - 30.10.2013)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT
- interní (30.10.2009 - 30.10.2013)

Odpovědnost: Kuncak Viktor