"Automata-based Verification of Programs with Tree Updates"@en . "248156" . . . "26230" . . . . "RIV/00216305:26230/10:PU89495!RIV11-GA0-26230___" . "Vojnar, Tom\u00E1\u0161" . "Automata-based Verification of Programs with Tree Updates" . . "31"^^ . . . "Formal verification, symbolic verification, programs handling balanced trees, theory of automata."@en . . "RIV/00216305:26230/10:PU89495" . . "Habermehl, Peter" . . . "Acta Informatica" . "This paper, which is an extended version of a paper originally published at TACAS'06, describes an effective verification procedure for imperative programs that handle (balanced) tree-like data structures. Since the verification problem considered is undecidable, we appeal to a classical semi-algorithmic approach in which the user has to provide manually the loop invariants in order to check the validity of Hoare triples of the form {P}C{Q}, where P, Q are the sets of states corresponding to the pre- and post-conditions, and C is the program to be verified. We specify the sets of states (representing tree-like memory configurations) using  a special class of tree automata named Tree Automata with Size Constraints (TASC). The main advantage of using TASC in program specifications is that they recognize non-regular sets of tree languages such as the AVL trees, the  red-black trees, and in general, specifications involving arithmetic reasoning about the lengths (depths) of various"@en . . "47" . "[4FF06F26DE1D]" . "Radu, Iosif" . "P(GA102/07/0322), Z(MSM0021630528)" . "1" . "Automata-based Verification of Programs with Tree Updates"@en . . . "This paper, which is an extended version of a paper originally published at TACAS'06, describes an effective verification procedure for imperative programs that handle (balanced) tree-like data structures. Since the verification problem considered is undecidable, we appeal to a classical semi-algorithmic approach in which the user has to provide manually the loop invariants in order to check the validity of Hoare triples of the form {P}C{Q}, where P, Q are the sets of states corresponding to the pre- and post-conditions, and C is the program to be verified. We specify the sets of states (representing tree-like memory configurations) using  a special class of tree automata named Tree Automata with Size Constraints (TASC). The main advantage of using TASC in program specifications is that they recognize non-regular sets of tree languages such as the AVL trees, the  red-black trees, and in general, specifications involving arithmetic reasoning about the lengths (depths) of various" . . "0001-5903" . "3"^^ . "DE - Spolkov\u00E1 republika N\u011Bmecko" . . "1"^^ . . "Automata-based Verification of Programs with Tree Updates" .