"1"^^ . . "0"^^ . . . "2008-01-01+01:00"^^ . . . "7"^^ . "435"^^ . "7"^^ . "formal verification; model checking; infinite systems; temporal logics"@en . "435"^^ . "2010-12-31+01:00"^^ . "Procesy ov\u011B\u0159ov\u00E1n\u00ED a garance kvality zalo\u017Een\u00E9 p\u0159ev\u00E1\u017En\u011B na pr\u00E1ci lid\u00ED nejsou vhodn\u00E9 pro v\u00FDvoj dne\u0161n\u00EDch rozs\u00E1hl\u00FDch hardwarov\u00FDch a softwarov\u00FDch syst\u00E9m\u016F. Perspektivn\u00EDm \u0159e\u0161en\u00EDm je pou\u017Eit\u00ED automatizovan\u00FDch n\u00E1stroj\u016F pro form\u00E1ln\u00ED verifikaci syst\u00E9m\u016F. A pr\u00E1v\u011B v\u00FDzkum v oblasti automatick\u00E9 form\u00E1ln\u00ED verifikace je t\u00E9matem p\u0159edkl\u00E1dan\u00E9ho projektu. Navrhovatel se chce konkr\u00E9tn\u011B zam\u011B\u0159it na t\u0159i oblasti: vlastnosti tempor\u00E1ln\u00EDch logik a vyu\u017Eit\u00ED t\u011Bchto vlastnost\u00ED p\u0159i konstrukci nov\u00FDch a vylep\u0161en\u00ED st\u00E1vaj\u00EDc\u00EDch verifika\u010Dn\u00EDch algoritm\u016F, vlastnosti formalism\u016F pro popis nekone\u010Dn\u011B stavov\u00FDch syst\u00E9m\u016F - jejich vyjad\u0159ovac\u00ED s\u00EDla a rozhodnutelnost z\u00E1kladn\u00EDch verifika\u010Dn\u00EDch probl\u00E9m\u016F pro odpov\u00EDdaj\u00EDc\u00ED t\u0159\u00EDdy nekone\u010Dn\u011B stavov\u00FDch syst\u00E9m\u016F, progresivn\u00ED sm\u011Bry ve verifikaci softwaru - zejm\u00E9na verifikace vlastnost\u00ED souvisej\u00EDc\u00EDch s dynamicky alokovanou pam\u011Bt\u00ED a aplikace verifika\u010Dn\u00EDch technik na b\u011B\u017En\u00E9 programovac\u00ED jazyky. V\u00FDstupem projektu budou publikace v mezin\u00E1rodn\u00EDch \u010Dasopisech a na mezin\u00E1rodn\u00EDch konferenc\u00EDch a"@cs . . "Formal verification: algorithms, properties of modelling formalisms and temporal logics"@en . . "0"^^ . . "Form\u00E1ln\u00ED verifikace: algoritmy, vlastnosti modelovac\u00EDch formalism\u016F a tempor\u00E1ln\u00EDch logik"@cs . . . "Quality assurance processes based mainly on humans are not suitable for development of current extensive hardware and software systems. Application of automatic verification tools is a promising solution. Research in the area of automatic formal verification is the aim of the proposed project. More precisely, the proposer intends to focus on the following three areas. Properties of temporal logics and aplication of these properties to development of new or improvement of the current verificationalgorithms properties of formalisms for modeling infinite-state systems - their expressive power and decidability of basic verification problems for the corresponding classes of infinite-state systems progressive directions in software verifications - inparticular verification of properties related to dynamic memory allocation and applications of verification techiques to common programming languages. The output of this research project will be papers in international journals and papers at"@en .