. "Vojnar, Tom\u00E1\u0161" . "3"^^ . "[ABB3B51D3090]" . "Automata-based Verification of Programs with Tree Updates"@en . . . "1"^^ . "466375" . "P(GA102/04/0780), P(GP102/03/D211)" . . "This paper 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 (possibly all) paths in the tree. The class of TASC is closed under the op" . . "Tools and Algorithms for the Construction and Analysis of Systems" . "Habermehl, Peter" . . "15"^^ . "This paper 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 (possibly all) paths in the tree. The class of TASC is closed under the op"@en . . "2006-03-25+01:00"^^ . . "Springer-Verlag" . "Automata-based Verification of Programs with Tree Updates" . . "Automata-based Verification of Programs with Tree Updates" . "Radu, Iosif" . . . . . "978-3-540-33056-1" . "RIV/00216305:26230/06:PU66868!RIV10-GA0-26230___" . "Automata-based Verification of Programs with Tree Updates"@en . . . . . "Formal verification, symbolic verification, programs handling balanced trees, theory of automata.
"@en . "26230" . "Berlin" . "Vienna" . "RIV/00216305:26230/06:PU66868" . .