|
|
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.
|
|
| |
|
|
Human Interface to Automata Libraries of MONA Tool
Pyšný, Radek ; Šimáček, Jiří (referee) ; Rogalewicz, Adam (advisor)
Finite tree automata is formalism used in many different areas of computer science, among others in the area of formal verification. Nowdays there are few tools used for handling of finite tree automata, however libraries of MONA tool are the best choice. The finite tree automata are a frequent tool for formal verification of computer systems which work with dynamic data structures. The input format of finite tree automata for libraries of MONA tool is very difficult for humans because it is necessary to enter the move function of the finite tree automaton in a form of several multiterminal binary decision diagrams. The aim of this thesis is to design and implement tool to convert the finite set of move rules into internal format of the MONA tool.
|
|
|
Tool for Abstract Regular Model Checking
Chalk, Matěj ; Rogalewicz, Adam (referee) ; Hruška, Martin (advisor)
Formal verification methods offer a large potential to provide automated software correctness checking (based on sound mathematical roots), which is of vital importance. One such technique is abstract regular model checking, which encodes sets of reachable configurations and one-step transitions between them using finite automata and transducers, respectively. Though this method addresses problems that are undecidable in general, it facilitates termination in many practical cases, while also significantly reducing the state space explosion problem. This is achieved by accelerating the computation of reachability sets using incrementally refinable abstractions, while eliminating spurious counterexamples caused by overapproximation using a counterexample-guided abstraction refinement technique. The aim of this thesis is to create a well designed tool for abstract regular model checking, which has so far only been implemented in prototypes. The new tool will model systems using symbolic automata and transducers instead of their (less concise) classic alternatives.
|
|
|
A Verified Data Structures Library
Rychnovský, Jan ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
This bachelor thesis deals with a methodology of writing verified programs using the VCC tool. The mentioned methodology is based in the principle of extending the program code with additional annotations, which provide a specification of the desired functionality. The VCC tool then uses formal methods to check whether the source code is correct with respect to the given specification. The first part describes formal verification and three basic approaches to it. Subsequently, the satisfiability problems of propositional formulae (SAT) and formulae in theories of predicate logic (SMT) are described. Then the thesis describes the VCC verification tool, its functionality, methodology, syntax and semantics of commands of its intermediate annotation language BoogiePL. The second part of this thesis is focused on the design and implementation of a verified data structures library, which contains singly linked, doubly linked, and circular lists, a binary search tree and a Treiber's stack. The text concludes with a discussion of the learnt knowledge about the programming methodology based on writing verified code.
|
|
|
Library for Finite Automata and Transducers
Bieliková, Michaela ; Lengál, Ondřej (referee) ; Hruška, Martin (advisor)
Finite state automata are widely used in the field of computer science such as formal verification, system modelling, and natural language processing. However, the models representing the reality are complicated and can be defined upon big alphabets, or even infinite alphabets, and thus contain a lot of transitions. In these cases, using classical finite state automata is not very efficient. Symbolic automata are more concise by employing predicates as transition labels. Finite state transducers also have a wide range of application such as linguistics or formal verification. Symbolic transducers replace classic transition labels with two predicates, one for input symbols and one for output symbols. The goal of this thesis is to design a library for letter and symbolic automata and transducers which will be suitable for fast prototyping.
|
|
|
Incremental Inductive Coverability for Alternating Finite Automata
Vargovčík, Pavol ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
In this work, we propose a specialization of the inductive incremental coverability algorithm that solves alternating finite automata emptiness problem. We experiment with various design decisions, analyze them and prove their correctness. Even though the problem itself is PSpace-complete, we are focusing on making the decision of emptiness computationally feasible for some practical classes of applications. We have obtained interesting comparative results against state-of-the-art algorithms, especially in comparison with antichain-based algorithms.
|
|
|
Control System for an Automatic Assembly Line
Jakeš, Libor ; Beran,, Jan (referee) ; Hynčica, Ondřej (advisor)
This master’s thesis deals with programming of control system for an automatic assembly line rear seats of passenger cars. The theoretical part describes assembly line, PLC, robot, electric nutrunner and intelligent camera Sick. Practical part of the thesis characterizes created programs of assembly workplace control system. This part also explains creating a model of station and subsequent formal verification of basic safety and functional properties.
|
|
|
Feedback Hardware Functional Verification
Santa, Marek ; Kajan, Michal (referee) ; Kořenek, Jan (advisor)
In the development process of digital circuits, it is often not possible to avoid introducing errors into systems that are being developed. Early detection of such errors saves money and time. This project deals with automation of feedback in functional verification of various data processing components. The goal of automatic feedback is not only to shorten the time needed to verify the functionality of a system, but mainly to improve verification coverage of corner cases and thus increase the confidence in the verified system. General functional and formal verification principles and practices are discussed, coverage metrics are presented, limitations of both techniques are mentioned and room for improvement of current status is identified. Design of feedback verification environment using a genetic algorithm is described in detial. The verification results are summarized and evaluated.
|
|
|
Questa Capabilities Demonstration Set
Krajčír, Stanislav ; Kajan, Michal (referee) ; Zachariášová, Marcela (advisor)
This bachelor thesis deals with presentation of capabilities of verification platform Questa Static from Mentor Graphics company. The basic information about the principles of assertion based verification is provided in the beginning. The thesis describes Questa AutoCheck verification tool which is used for automatic verification of integrated circuits and Questa Formal verification tool which is used for static formal verification of integrated circuits. The set of examples is given to demonstrate various options of using these tools for verification of a concrete integrated circuit design. In conclusion, the thesis evaluates the possibilities of application of these tools in verification process.
|
guest ::
