Department of Intelligent Systems



AUFOVER - AuFoVer - Automated Formal Verification

Czech title:AuFoVer - Automatizace Formální Verifikace
Research leader:Kratochvíla Tomáš (Honeywell)
Team leaders:Smrčka Aleš
Team members:Vojnar Tomáš
Agency:Technology Agency of the Czech Republic
Code:TH04010192
Start:2019-01-01
End:2021-12-31
Keywords:formal verification; static analysis; symbolic verification; dynamic analysis and testing; model-based testing; automata; requirement specification; logics;
Annotation:
The main scope of the project is on reducing cost of development of critical systems by leveraging tools for automated formal verification. In particular, the project concentrates on (1) transparent deployment of formal methods (formal verification will be used in a way requiring minimal modification of current processes), (2) automated semantic analysis of requirements (requirements written in natual language wil be automatically formalised and system engineers will be able to gain information about inconsistent, duplicate, unrealisable, or missing requirements), and (3) automated formal verification of system wrt. requirements (the developers will be able to verify if an implementation in C/C++ satisfies a given requirements with no need to create abstract models of a verified system). The new developed methods and tools will be included in industrial practice to allow revealing bugs sooner in development cycle.

Your IPv4 address: 54.161.118.57