|
|
Statistické ověřování modelů přibližných výpočetních systémů
Blažek, Michal ; Sekanina, Lukáš (oponent) ; Strnadel, Josef (vedoucí práce)
Tato bakalářská práce se zaměřuje na statistické ověřování modelů přibližných násobiček. Zejména se zabývá srovnáním vlastností násobiček při generování jejich vstupních hodnot podle různých pravděpodobnostních rozdělení. Součástí práce je převod modelů násobiček z knihovny EvoApproxLib do modelů v prostředí UPPAAL. Vytvořené modely jsou poté simulovány s ohledem na vybrané hodnotící metriky, jako např. pravděpodobnost chyby, průměrná absolutní chyba aj. Ze získaných výsledků lze usuzovat, že použitím vhodné aproximační násobičky pro provádění výpočtů v rámci konkrétní aplikace je možné docílit menší chyby ve výpočtech. Výsledky by proto mohly mít další uplatnění v oblasti přibližných výpočetních systémů.
|
|
|
HyperLTL Model Checking
Alexaj, Ondrej ; Strejček, Jan (oponent) ; Lengál, Ondřej (vedoucí práce)
HyperLTL model checking is an approach to verifying a system against a given hyperproperty, which is able to relate multiple executions of a system. The algorithmic approach based on automata which relies on standard -automata operations is well established. The aim of this work is to outperform the complete state-of-the-art HyperLTL model checker AutoHyper by employing more efficient partial automata operations, in particular complementation and inclusion. The implementation of HyperLTL model checking in a novel modular-based complementation tool Kofola resulted in a significant enhancement in performance compared to the reference tool. Finally, our approach to language inclusion checking shows a notable improvement in terms of the generated state space. As a commonly used automata operation, it could potentially contribute to the advancement of other areas of verification.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (oponent) ; Veith, Helmut (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
The work presented in this thesis focuses on finite state automata over finite words and finite trees, and the use of such automata in formal verification of infinite-state systems. First, we focus on extensions of a previously introduced framework for verifi cation of heap-manipulating programs-in particular programs with complex dynamic data structures-based on tree automata. We propose several extensions to the framework, such as making it fully automated or extending it to consider ordering over data values. Further, we also propose novel decision procedures for two logics that are often used in formal verification: separation logic and weak monadic second order logic of one successor. These decision procedures are based on a translation of the problem into the domain of automata and subsequent manipulation in the target domain. Finally, we have also developed new approaches for efficient manipulation with tree automata, mainly for testing language inclusion and for handling automata with large alphabets, and implemented them in a library for general use. The developed algorithms are used as the key technology to make the above mentioned techniques feasible in practice.
|
|
|
Nástroj pro statickou analýzu programů se seznamy
Kotoun, Michal ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tvorba softwarového analyzátoru je komplexní úloha -- je nutno implementovat parsování zdrojového kódu, reprezentaci instrukcí, abstrakci hodnot, uživatelské rozhraní, ... a také analýzu samu. Abychom předešli zbytečné práci vývojářů analýz, rozhodli jsme se vytvořit framework pro statickou analýzu programů. Předkládáme obecný návrh frameworku zvaného Angie s důrazem na jeho použitelnost a popisujeme prototyp frameworku, včetně modelové analýzy založené na symbolických paměťových grafech. Angie je implementován v C++ a používá nástroje z kolekce LLVM pro parsování zdrojového kódu analyzovaných programů.
|
|
|
Efektivní algoritmy pro práci s konečnými automaty
Hruška, Martin ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Nedeterministické konečné automaty jsou používány v mnoha oblastech informatiky, mimo jiné také ve formální verifikaci, při návrhu číslicových obvodů nebo pro reprezentaci regulárlních jazyků. Jejich výhodou oproti deterministickým konečným automatům je schopnost až exponenciálně stručnější reprezentace jazyka. Nicméně, tato výhoda může být pozbyta, jestliže je zvolen naivní přístup k implementaci některých operací, jako je na\-pří\-klad test jazykové inkluze dvojice automatů, jehož naivní implementace provádí explicitní determinizaci jednoho z automatů. V nedávné době bylo ale představeno několik nových přístupů, které právě explicitní determinizaci při testu jazykové inkluze předcházejí. Tyto přístupy využívají tzv. antichainů nebo tzv. bisimulace vzhůru ke kongruenci. Cílém této práce je vytvoření efektivní implementace zmíněných přístupů v podobě nového rozšíření knihovny VATA. Vytvořená implementace byla otestována a je až řádově rychlejší v 90% testovaných případů nežli implementace jiné
|
|
|
Překladač grafu toků dat do logiky bitových vektorů
Sušovský, Tomáš ; Lengál, Ondřej (oponent) ; Smrčka, Aleš (vedoucí práce)
Cílem této bakalářské práce je vytvořit a implementovat nástroj pro překlad modelů grafů toků dat do formátu SMT-LIB. Práce navazuje na projekt HADES výzkumné skupiny VeriFIT Fakulty informačních technologií Vysokého učení technického v Brně. V řešení bylo použito překladače vytvářejícího z původního grafu objektový model. Objektový model je možné převést do zápisu ve formátu SMT-LIB a přidat do něj aserce požadovaných vlastností systému. Pro ověřování vlastností závisejících na změnách systému je použita metoda rozbalování smyček s uživatelem zadanou hranicí maximálního počtu rozbalení. Možnosti vytvořeného nástoje jsou demonstrovány na sadě modelů grafů toků dat pokrývající všechny prvky vstupního jazyka VAM a jejich kombinace. Výsledek této práce představuje nové možnosti pro zpracování grafů toků dat ve formátu VAM a jejich verifikaci.
|
|
|
Dynamická detekce a léčení časově závislých chyb nad daty v prostředí Java
Letko, Zdeněk ; Kolář, Dušan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Hledání chyb plynoucích ze souběžného zpracovávání výpočtů je obtížné. Proto se tato diplomová práce zabývá detekcí a léčením časově závislých chyb nad daty a chyb plynoucích z nesprávné atomicity operací v prostředí Java. Práce prezentuje dva různé algoritmy pro detekci. Jedním z nich je nový algoritmus nazvaný AtomRace, který detekuje časově závislé chyby nad daty jako speciální případ nesprávné atomicity operací. Následné léčení detekovaných chyb je založeno na potlačení opakování chyby, buď zavedením přídavné synchronizace, nebo legálním ovlivňováním plánovače Javy, za účelem vynucení správné atomicity operací. Navržená architektura, která pracuje souběžně se sledovaným programem, využívá ke sledování a ovlivňování výpočtu techniku instrumentace na úrovni Java bytecode. Architektura a algoritmy byly implementovány a otestovány v několika případových studiích.
|
|
|
Generic Template-Based Synthesis of Program Abstractions
Marušák, Matej ; Holík, Lukáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to design and to implement a generic strategy solver to the 2LS tool. 2LS is an analyser for a static verification of programs written in C language. A verified program is analysed by an SMT solver using abstract interpretation. Convertion from an abstract state of the program into a logical formula, that an SMT solver can work with, is done by a component called strategy solver. In the current implementation, there is one strategy solver for each abstract domain. Our approach introduces a single generic strategy solver, which makes creating new domains easier. Also, this approach enables migration of the existing domains and hence the codebase can be reduced.
|
|
| |
|
|
Lidské rozhraní k automatovým knihovnám nástroje MONA
Pyšný, Radek ; Šimáček, Jiří (oponent) ; Rogalewicz, Adam (vedoucí práce)
Konečné stromové automaty jsou formalismem používaným v mnoha různých oblastech informatiky, mimo jiné v oblasti formální verifikace. V současné době existuje několik nástrojů pro práci s konečnými stromovými automaty, avšak knihovny nástroje MONA jsou pro tyto účely nejlepší. Právě konečné stromové automaty jsou častým nástrojem pro formální verifikaci počítačových systémů, které pracují s dynamickými datovými strukturami. Způsob, jakým je realizováno zadávání konečných stromových automatů pro knihovny nástroje MONA , je pro člověka značně náročný, protože je nutné funkci přechodu konečného stromového automatu zadat ve formě několika multiterminálních binárních rozhodovacích diagramů. Cílem této diplomové práce je navrhnout a implementovat nástroj pro převod konečných stromových automatů zapsaných výčtem pravidel do interního formátu nástroje MONA .
|
host ::
RSS.