. "Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures"@en . "Hol\u00EDk, Luk\u00E1\u0161" . "Anal\u00FDza protip\u0159\u00EDklad\u016F v abstraktn\u00EDm regul\u00E1rn\u00EDm model checkingu pro slo\u017Eit\u00E9 dynamick\u00E9 datov\u00E9 struktury"@cs . . "26230" . "Formal verification, Regular tree model checking, shape analysis,
"@en . . "P(GD102/05/H050), Z(MSM0021630528)" . . . . . . "Anal\u00FDza protip\u0159\u00EDklad\u016F v abstraktn\u00EDm regul\u00E1rn\u00EDm model checkingu pro slo\u017Eit\u00E9 dynamick\u00E9 datov\u00E9 struktury"@cs . . "We focus in details on the use of abstract regular tree model checking (ARTMC) within a successful method for verification of programs with dynamic data structures. The method is based on a use of a set of transducers to describe the behaviour of the verified system. But the ARTMC method was originally developed for systems of one transducer only and its generalization to several ones was supposed to be straightforward. Although this straightforward generalization (used in a prototype  implementation) works well in a number of examples, the counterexample analysis is in general unreliable and can cause infinite looping of the tool as we demonstrate on a simple example containing an erroneous pointer manipulation. Therefore we propose a new  algorithm used for a counterexample analysis and we prove its correctness."@en . "2"^^ . . "2"^^ . "We focus in details on the use of abstract regular tree model checking (ARTMC) within a successful method for verification of programs with dynamic data structures. The method is based on a use of a set of transducers to describe the behaviour of the verified system. But the ARTMC method was originally developed for systems of one transducer only and its generalization to several ones was supposed to be straightforward. Although this straightforward generalization (used in a prototype  implementation) works well in a number of examples, the counterexample analysis is in general unreliable and can cause infinite looping of the tool as we demonstrate on a simple example containing an erroneous pointer manipulation. Therefore we propose a new  algorithm used for a counterexample analysis and we prove its correctness." . "RIV/00216305:26230/07:PU70921!RIV08-MSM-26230___" . "Neuveden" . . "[5016F15BF99A]" . . "Third Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007)" . . . . "2007-10-26+02:00"^^ . "Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures" . "Rogalewicz, Adam" . . . . "Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures"@en . . "RIV/00216305:26230/07:PU70921" . "59-66" . "Counterexample Analysis in Abstract Regular Tree Model Checking of Complex Dynamic Data Structures" . "415189" . . "Znojmo" . "\u010Cl\u00E1nek studuje pou\u017Eit\u00ED abstraktn\u00EDho regul\u00E1rn\u00EDho model checkingu, uvnit\u0159 \u00FAsp\u011B\u0161n\u00E9 metody pro verifikace program\u016F se slo\u017Eit\u00FDmi datov\u00FDmi strukturami, a to zejm\u00E9na anal\u00FDza protip\u0159\u00EDklad\u016F.
"@cs . "Znojmo" . "8"^^ . "978-80-7355-077-6" .