. . . "Abstract Regular Tree Model Checking of Complex Dynamic Data Structures"@en . "Verifikace komplexn\u00EDch dynamick\u00FDch datov\u00FDch struktur za pou\u017Eit\u00EDm abstraktn\u00EDho regul\u00E1rn\u00EDho stromov\u00E9ho model checkingu"@cs . . "Habermehl, Peter" . "Springer-Verlag" . . "P(GA102/04/0780), P(GD102/05/H050), P(GP102/03/D211)" . . "Abstract Regular Tree Model Checking of Complex Dynamic Data Structures" . . "Formal verification, symbolic verification, shape analysis, dynamic data structures, tree automata.
"@en . . "2"^^ . "Abstract Regular Tree Model Checking of Complex Dynamic Data Structures" . . "2006-08-29+02:00"^^ . . . "Vojnar, Tom\u00E1\u0161" . . "4"^^ . "Bouajjani, Ahmed" . "Rogalewicz, Adam" . . . "26230" . "463962" . . "Seoul" . . "[51C75C3AE984]" . "Berlin" . "We consider the verification of non-recursive C programs manipulating dynamic linked data structures with possibly several next pointer selectors and with finite domain non-pointer data. We aim at checking basic memory consistency properties (no null pointer assignments, etc.) and shape invariants whose violation can be expressed in an existential fragment of a first order logic over graphs. We formalise this fragment as a logic for specifying bad memory patterns whose formulae may be translated to testers written in C that can be attached to the program, thus reducing the verification problem considered to checking reachability of an error control line. We encode configurations of programs, which are essentially shape graphs, in an original way as extended tree automata and we represent program statements by tree transducers. Then, we use the abstract regular tree model checking framework for a fully automated verification. The method has been implemented and successfully applied on several case stud" . "RIV/00216305:26230/06:PU66952!RIV07-GA0-26230___" . "Verifikace komplexn\u00EDch dynamick\u00FDch datov\u00FDch struktur za pou\u017Eit\u00EDm abstraktn\u00EDho regul\u00E1rn\u00EDho stromov\u00E9ho model checkingu"@cs . . "RIV/00216305:26230/06:PU66952" . "52-69" . . . . "\u010Cl\u00E1nek se zab\u00FDv\u00E1 verifikac\u00ED program\u016F pracuj\u00EDc\u00EDch s dynamick\u00FDmi datov\u00FDmi strukturami. Ka\u017Ed\u00FD uzel m\u016F\u017Ee obsahovat n\u011Bkolik ukazatel\u016F na n\u00E1sleduj\u00EDc\u00ED uzly a datovou hodnotu z kone\u010Dn\u00E9 mno\u017Einy datov\u00FDch hodnot. Kontrolujeme zak\u00E1zan\u00E9 manipulace s nulov\u00FDmi a nedefinovan\u00FDmi ukazateli, a d\u00E1le i tvarov\u00E9 vlastnosti (shape properties) datov\u00E9 struktury. Pro specifikaci t\u011Bchto vlastnost\u00ED pou\u017E\u00EDv\u00E1me fragment first-order logiky nad grafy. Zak\u00E1zan\u00E9 stavy popsan\u00E9 v t\u00E9to logice lze automaticky p\u0159ev\u00E9st do C programu, kter\u00FD je p\u0159id\u00E1n na konec verifikovan\u00E9ho programu. T\u00EDmto p\u0159evedeme problem kontroly datov\u00E9 struktury na problem dosa\u017Eitelnosti dan\u00E9 \u0159\u00E1dky v programu. Konfigurace programu, kter\u00E9 jsou orientovan\u00FDmi grafy k\u00F3dujeme jako roz\u0161\u00ED\u0159en\u00E9 stromov\u00E9 automaty, a p\u0159\u00EDkazy programu jako stromov\u00E9 p\u0159evodn\u00EDky. Pot\u00E9 m\u016F\u017Eeme vyu\u017E\u00EDt metodu abstract regular tree model checking pro automatickou verifikaci t\u011Bchto program\u016F. Kompletn\u00ED metoda byla implementov\u00E1na v prototy"@cs . . "We consider the verification of non-recursive C programs manipulating dynamic linked data structures with possibly several next pointer selectors and with finite domain non-pointer data. We aim at checking basic memory consistency properties (no null pointer assignments, etc.) and shape invariants whose violation can be expressed in an existential fragment of a first order logic over graphs. We formalise this fragment as a logic for specifying bad memory patterns whose formulae may be translated to testers written in C that can be attached to the program, thus reducing the verification problem considered to checking reachability of an error control line. We encode configurations of programs, which are essentially shape graphs, in an original way as extended tree automata and we represent program statements by tree transducers. Then, we use the abstract regular tree model checking framework for a fully automated verification. The method has been implemented and successfully applied on several case stud"@en . "3-540-37756-5" . "18"^^ . "Abstract Regular Tree Model Checking of Complex Dynamic Data Structures"@en . "Static Analysis" .