"verification engineering automated verification of programs static and dynamic analysis formal verification model checking concurrency multicore processors infinite-state programs dynamic data structures"@en . . . "Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness"@en . "2013-06-12+02:00"^^ . . "The project has brought internationally recognized results in the formal verification of programs with various sources of unboundedness and of concurrent programs. These were high quality publications in journals (7) and at international conferences (31), as well as publicly available software tools for experiments in program verification. Three conference papers received a best paper award."@en . "Automatizovan\u00E1 verifikace program\u016F je v sou\u010Dasnosti s ohledem na rostouc\u00ED dopad po\u010D\u00EDta\u010Dem \u0159\u00EDzen\u00FDch syst\u00E9m\u016F na na\u0161e \u017Eivoty a v\u00FDraznou pot\u0159ebu minimalizovat po\u010Det chyb v t\u011Bchto syst\u00E9mech velmi aktu\u00E1ln\u00EDm v\u00FDzkumn\u00FDm t\u00E9matem. Projekt se konkr\u00E9tn\u011B zam\u011B\u0159uje na verifikaci program\u016F s pokro\u010Dil\u00FDmi rysy paralelismu a neomezenosti, kter\u00E9 pat\u0159\u00ED k obzvl\u00E1\u0161t\u011B problematick\u00FDm aspekt\u016Fm software, se kter\u00FDmi se mus\u00ED automatick\u00E1 verifikace vyrovn\u00E1vat. V prvn\u00EDm p\u0159\u00EDpad\u011B se projekt soust\u0159e\u010Fuje zejm\u00E9na na metody verifikace program\u016F ur\u010Den\u00FDch pro modern\u00ED v\u00EDcej\u00E1drov\u00E9 procesory. V druh\u00E9m p\u0159\u00EDpad\u011B se jedn\u00E1 o verifikaci program\u016F pracuj\u00EDc\u00EDch s r\u016Fzn\u00FDmi neomezen\u00FDmi datov\u00FDmi strukturami, zejm\u00E9na pak poli (o parametrick\u00E9 velikosti) a slo\u017Eit\u00FDmi dynamick\u00FDmi strukturami zalo\u017Een\u00FDmi na ukazatel\u00EDch (jako jsou seznamy \u010Di stromy). Projekt zahrnuje v\u00FDzkum metod dynamick\u00E9 i statick\u00E9 verifikace, v\u010Detn\u011B model checkingu, a tak\u00E9 jej\u00EDch vhodn\u00FDch kombinac\u00ED. Pro pr\u00E1ci s programy s nekone\u010Dn\u00FDmi stavov\u00FDmi prostory se v\u00FDzkum v projektu zam\u011B\u0159uje na metody efektivn\u00ED symbolick\u00E9 verifikace zalo\u017Een\u00E9 na pou\u017Eit\u00ED automat\u016F a logik." . "Projekt p\u0159inesl mezin\u00E1rodn\u011B v\u00FDznamn\u00E9 v\u00FDsledky ve form\u00E1ln\u00ED verifikaci program\u016F s r\u016Fzn\u00FDmi zdroji neomezenosti a paraleln\u00EDch program\u016F. T\u011Bmi byly vysoce kvalitn\u00ED publikace v \u010Dasopisech (7) a na mezin\u00E1rodn\u00EDch konferenc\u00EDch (31), jako\u017E i ve\u0159ejn\u011B dostupn\u00E9 softwarov\u00E9 n\u00E1stroje pro experimenty v oblasti verifikace program\u016F. T\u0159i konferen\u010Dn\u00ED \u010Dl\u00E1nky z\u00EDskaly ocen\u011Bn\u00ED za nejlep\u0161\u00ED \u010Dl\u00E1nek."@cs . "63"^^ . "2014-07-01+02:00"^^ . "2010-01-01+01:00"^^ . . "1"^^ . "63"^^ . "Statick\u00E1 a dynamick\u00E1 verifikace program\u016F s pokro\u010Dil\u00FDmi rysy paralelismu a neomezenosti" . . . . "0"^^ . "0"^^ . . . . . . "Automated verification of programs is currently a very hot issue due to the rising influence of computer-controlled systems on our lives and the recognised need to minimise the number of errors in them. The project, in particular, considers verification of programs with advanced features of concurrency and unboundedness, which both belong among especially problematic features to be dealt with in automated verification. In the former case, the project pays a special attention to verification of applications intended to run on the current multi-core processors. In the latter case, verification of programs manipulating different unbounded structures, notably (parameterised-size) arrays and complex dynamic linked data structures (such as lists or trees), is considered. The project contains research on methods of dynamic as well as static verification, including model checking, and possibly their suitable combinations. For handling infinite-state programs, efficient symbolic verification methods based on automata and logics are the primary target of the research in the project."@en . . . . . . "GAP103/10/0306" . . . "http://www.isvav.cz/projectDetail.do?rowId=GAP103/10/0306"^^ . "2013-12-31+01:00"^^ .