|
|
Generic Template-Based Synthesis of Program Abstractions
Marušák, Matej ; Holík, Lukáš (referee) ; Malík, Viktor (advisor)
Cieľom tejto práce je návrh a implementácia generického strategy solveru pre nástroj 2LS. 2LS je analyzátor na statickú verifikáciu programov napísaných v jazyku C. Verifikovaný program je za využita abstraktnej interpretácie analyzovaný SMT solverom. Prevod z ab- straktného stavu programu do logickej formule, s ktorou vie pracovať SMT solver vykonáva komponenta nazývaná strategy solver. Aktuálne pre každú doménu existuje jeden takýto solver. Navrhované riešenie vytvára jeden obecný strategy solver, ktorý zjednodušuje tvorbu nových domén. Zároveň navrhovaný spôsob umožnuje prevedenie existujúcich domén a teda zmenšuje program analyzátora.
|
|
|
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.
|
|
|
Generic Template-Based Synthesis of Program Abstractions
Marušák, Matej ; Holík, Lukáš (referee) ; Malík, Viktor (advisor)
Cieľom tejto práce je návrh a implementácia generického strategy solveru pre nástroj 2LS. 2LS je analyzátor na statickú verifikáciu programov napísaných v jazyku C. Verifikovaný program je za využita abstraktnej interpretácie analyzovaný SMT solverom. Prevod z ab- straktného stavu programu do logickej formule, s ktorou vie pracovať SMT solver vykonáva komponenta nazývaná strategy solver. Aktuálne pre každú doménu existuje jeden takýto solver. Navrhované riešenie vytvára jeden obecný strategy solver, ktorý zjednodušuje tvorbu nových domén. Zároveň navrhovaný spôsob umožnuje prevedenie existujúcich domén a teda zmenšuje program analyzátora.
|
|
|
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.
|
guest ::
