|
|
An Efficient Functional Library for Finite Automata
Říha, Jakub ; Hruška, Martin (referee) ; Lengál, Ondřej (advisor)
Finite automata are an important mathematical abstraction, and in formal verification, they are used for a concise representation of regular languages. Operations often used on finite automata in this setting are testing their universality and language inclusion. \mbox{A naive} approach to implement these operations leads to an explicit determinization of the automata, which can be costly and undesirable. There is, however, a more advanced method for performing those operations, called the Antichains algorithm, which avoids such an explicit determinization. This work shows how finite automata operations can be effectively implemented in Haskell and compares several approaches of their implementation. The obtained results are compared with VATA, an imperative implementation of a finite automata library.
|
|
|
Employing Approximate Equivalence for Design of Approximate Circuits
Matyáš, Jiří ; Lengál, Ondřej (referee) ; Češka, Milan (advisor)
This thesis is concerned with the utilization of formal verification techniques in the design of the functional approximations of combinational circuits. We thoroughly study the existing formal approaches for the approximate equivalence checking and their utilization in the approximate circuit development. We present a new method that integrates the formal techniques into the Cartesian Genetic Programming. The key idea of our approach is to employ a new search strategy that drives the evolution towards promptly verifiable candidate solutions. The proposed method was implemented within ABC synthesis tool. Various parameters of the search strategy were examined and the algorithm's performance was evaluated on the functional approximations of multipliers and adders with operand widths up to 32 and 128 bits respectively. Achieved results show an unprecedented scalability of our approach.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
|
|
|
Data Structure Visualization for Verification Tools
Holubec, Michael ; Lengál, Ondřej (referee) ; Peringer, Petr (advisor)
The aim of my bachelor thesis is an object-oriented design and implementation of a library which will provide a unified interface to a verification tool Predator and other tools for making a vizualization of data structures primarily for debuging purposes. This work analyses some qualities of the verification tool Predator, Forester and CPAchecker. The library offers not only a graphic but also a text-based output in DOT language. The result has been tested by connecting to the verification tool Predator.
|
|
|
A Bit-Vector Compiler for Data-Flow Graphs
Sušovský, Tomáš ; Lengál, Ondřej (referee) ; Smrčka, Aleš (advisor)
The principal goal of this bachelor thesis is to design and implement a tool for compiling data-flow graph models to SMT-LIB format. This thesis builds on the research project HADES developed by VeriFIT research group of the Faculty of Information Technology, Brno University of Technology. The solution uses compiler for generating object model from original graph. Object model can be converted to a SMT-LIB format description including assertions of the desired system properties. Loop unrolling method (with user defined boundary for unrollment) is used for verification of system properties depending on changes in state of model. Capabilities of the developed tool are demonstrated on set of data-flow graphs models. Models cover usage of all elements defined in VAM language (input format) and their combinations. Result of this thesis presents new ways of processing data-flow graphs in VAM format and their verification.
|
|
|
Static Behavioral Malware Detection over LLVM IR
Surovič, Marek ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá metodami pro behaviorální detekci malware, které využívají techniky formální analýzy a verifikace. Základem je odvozování stromových automatů z grafů závislostí systémových volání, které jsou získány pomocí statické analýzy LLVM IR. V rámci práce je implementován prototyp detektoru, který využívá překladačovou infrastrukturu LLVM. Pro experimentální ověření detektoru je použit překladač jazyka C/C++, který je schopen generovat mutace malware za pomoci obfuskujících transformací. Výsledky předběžných experimentů a případná budoucí rozšíření detektoru jsou diskutovány v závěru práce.
|
|
|
Data Structures with Paralell Access
Opletal, Tomáš ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Parallel programming brings out, apart from the opportunity to spread out a program execution to many simultaneously running processes sharing data, some new problems. It is necessary to synchronize these processes running in parallel and make sure that during the process communication and data sharing there will not arise any troubles. These synchronization algorithms also cannot use too much resources that are otherwise used for the actual program. This thesis describes ways of process synchronization and also provides an implementation of several algorithms for parallel queue. Implemented algorithms were also tested for their performance.
|
|
|
Symbolic Representation of Finite Automata
Chromečka, Jiří ; Vojnar, Tomáš (referee) ; Lengál, Ondřej (advisor)
In formal analysis we often encounter finite automata with a~large amount of states over large alphabets. Their explicit representation can result in a~state explosion and this problem can be solved by the use of symbolic representation that can manipulate a~whole set of states at once. The aim of this work is to extend the libVATA library to support such a~representation including algorithms for some operations on this representation. The presented text first deals with prerequisites necessary to undestand finite automata and binary decision diagrams used for their symbolic representation. Then it lists some existing libraries for work with finite automata. Next follows the core of this work, the~design of a~symbolic representation and operations on it, which are later implemented in the previously mentioned library. The test results proves that the symbolic representation is an interesting alternative to the explicit representation.
|
|
|
Static Analysis for Discovering Security Vulnerabilities in Web Applications on the Asp.Net Platform
Říha, Jakub ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor)
Tato bakalářská práce popisuje jak teoretické základy, tak způsob vytvoření statického analyzátoru založeném na platformě .NET Framework a službách poskytnutých prostřednictvím .NET Compiler Platform. Tento analyzátor detekuje bezpečnostní slabiny typu SQL injection na platformě ASP.NET MVC. Analyzátor nejdříve sestrojuje grafy řízení toku jako abstraktní reprezentaci analyzovaného programu. Poté využívá statické analýzy pro sledování potenciálně nedůvěryhodných dat. Nakonec jsou výsledky analýzy prezentovány uživateli.
|
|
|
A BDD Library
Troška, Karol ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
Binary decision program is a data structure used in many areas of information technology. This thesis describes BDD as a mathematical formalism and proposes possible representation of BDD in a computer. The propose is focused mainly on a reduction speed of number of memory allocation and on a simplicity and an intuitive system of using a library. There are several examples of a library usage and warnings which programmer should avoid of in the thesis. Proposed representation was implemented in C language.
|
guest ::
