|
|
Tool for Abstract Regular Tree Model Checking
Mráz, Patrik ; Rogalewicz, Adam (referee) ; Hruška, Martin (advisor)
Formal verification deals with proving the correctness of the system according to the given specifications. Its need is driven by an increasing number of computers and a increase in the complexity of the systems being developed. The aim of this work is to implement the formal verification tool abstract regular tree model checking (ARTMC) over the VATA library. To achieve this goal, it was necessary to extend the VATA library on the finite tree transducers, abstractions of tree automata and integrate them together with the ARTMC into the VATA library.
|
|
|
Compiler of C Language Fragment to ARTMC Tool
Marušák, Matej ; Hruška, Martin (referee) ; Rogalewicz, Adam (advisor)
Abstract With growing complexity of software programs the need for automated analysis and verifi- cation grows as well. Reasearch group VeriFIT based on Faculty of Information Technology of Brno University of Technology is involved in research of this area. One of the developed tools is the ARTMC tool. This bachelor’s thesis designs and implements compiler of C lan- guage fragment into input format of the ARTMC tool. Implemented compiler makes work with ARTMC tool much easier, since the input format is not suitable for manual creation.
|
|
|
Compiler of C Language Fragment to ARTMC Tool
Marušák, Matej ; Hruška, Martin (referee) ; Rogalewicz, Adam (advisor)
Abstract With growing complexity of software programs the need for automated analysis and verifi- cation grows as well. Reasearch group VeriFIT based on Faculty of Information Technology of Brno University of Technology is involved in research of this area. One of the developed tools is the ARTMC tool. This bachelor’s thesis designs and implements compiler of C lan- guage fragment into input format of the ARTMC tool. Implemented compiler makes work with ARTMC tool much easier, since the input format is not suitable for manual creation.
|
|
|
Tool for Abstract Regular Tree Model Checking
Mráz, Patrik ; Rogalewicz, Adam (referee) ; Hruška, Martin (advisor)
Formal verification deals with proving the correctness of the system according to the given specifications. Its need is driven by an increasing number of computers and a increase in the complexity of the systems being developed. The aim of this work is to implement the formal verification tool abstract regular tree model checking (ARTMC) over the VATA library. To achieve this goal, it was necessary to extend the VATA library on the finite tree transducers, abstractions of tree automata and integrate them together with the ARTMC into the VATA library.
|
guest ::
