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.

Description in Czech
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ů.

Keywords
formal modelling, formal verification, decision procedures, synthesis

IC0901

English

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

Department of Intelligent Systems
- responsible department (28.11.2009 - not assigned)
Automated Analysis and Verification Research Group - VeriFIT
- internal (30.10.2009 - 30.10.2013)
Security-aware research in information technology
- internal (30.10.2009 - 30.10.2013)

Responsibility: Kuncak Viktor