Automatizace formální verifikace

formal verification; static analysis; symbolic verification; dynamic analysis and
testing; model-based testing; automata; requirement specification; logics;

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.