|
|
Heuristics in String Solving
Řezáč, Michal ; Havlena, Vojtěch (referee) ; Síč, Juraj (advisor)
Tato práce se zaměřuje na identifikaci heuristik a strategií použitých v moderních string solverech a na vyhodnocení jejich dopadu na efektivitu řešení. Zkoumány jsou především dva solvery – cvc5 a Z3. Práce popisuje techniky používané SMT solverech a strategie, které implementují string solvery. Vyhodnocení efektivity heuristik bylo prováděno jejich vypínáním přímo v kódu uvedených nástrojů a následným vyhodnocením dopadu na řešení standardních sad benchmarků. Výsledkem této práce je soupis sady konkrétních heuristik a popis struktury nástrojů cvc5 a Z3. Měřením se nepodařilo prokázat, jak velký skutečný dopad identifikované a popsané heuristiky mají.
|
|
|
Transducers in Automata Library Mata
Chocholatý, David ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Implementujeme konečné převodníky do nové rychlé a jednoduché automatové knihovny Mata. Konečné převodníky jsou konečné stavové stoje modelující regulární relace. Naše hlavní použití pro konečné převodníky je kódovaní operací nahrazení (nahrazení slova nebo regulárního vzoru řetězcem). Nový SMT nástroj pro řešení formulí s omezeními nad řetězci Z3-Noodler používá knihovnu Mata jako základ pro jeho rozhodovací proceduru. Noodler potřebuje konečné převodníky k analýze programů manipulujících s řetězci s operacemi nahrazení. Analýzou zmíněných programů používaných ve webových aplikacích se zabrání útokům jako cross-site scripting (XSS) nebo vložení kódu. Hlavní odlišující vlastnosti knihovny Mata zahrnují jednoduchost (jednoduchá k užívání, úpravě a rozšíření) a efektivitu (pracuje rychle). Reprezentaci a algoritmy pro konečné převodníky jsme navrhli s ohledem na tyto vlastnosti knihovny. K reprezentaci konečných převodníků a jejich algoritmů znovupoužijeme a rozšíříme existující datové struktury a algoritmy pro konečné automaty v knihovně Mata. Reprezentace pro konečné převodníky slouží jako společná reprezentace pro konečné převodníky a budoucí reprezentaci automatů využívajících multi-terminálních binárních rozhodovacích diagramů pro práci s velkými abecedami. Navíc rozšíříme návrh o algoritmy pro konstrukci konečných převodníků modelujících operace nahrazení definovaných v SMT-LIB. Nakonec experimentálně vyhodnotíme efektivitu konečných převodníků v knihovně Mata na nové sadě příkladů s operacemi nahrazení z běhů nástroje Z3-Noodler a z řešení problémů nalezení vzoru.
|
|
|
Modernization of Tenryu Pick and Place Machine
Drška, Jan ; Szabó, Zoltán (referee) ; Mikulka, Jan (advisor)
The aim of the diploma thesis is to evaluate the current state of the machine and to propose a possible solution for the modernization of the machine and to implement selected parts. The thesis includes documentation of the original state of the Tenryu MT-5530LQ automatic machine and its documentation after modernization. In the introductory part, the theory of the automatic machine is described, this chapter is followed by a description of the function and design of the aforementioned machine. The third chapter describes and identifies the machine components that need to be replaced or repaired. The fourth chapter of this thesis contains a complete proposal for the modernization of the machine, including the possible results of the modernization. These previous chapters are followed by chapters 5, 6 and 7 where new cards for the proposed control system are described and the thesis concludes with a summary of the impact of the upgrade on the machine including options for continuing to upgrade the machine.
|
|
|
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.
|
|
|
PCBs Repairs with BGA and FC Packages
Buřival, Tomáš ; Špinka, Jiří (referee) ; Starý, Jiří (advisor)
Graduation thesis is specialized on dilemma of the integrated circuits with ball grid array. Chapter two describes several types of packages and confrontation of their characteristics. Chapter three considers possibilities of corrections these boards bedded with packages, mounting and demounting of these packages, method of camera control and also inspection of the soldering process. Chapter four attend to practical measuring of thermal profiles and their optimalization.
|
|
|
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.
|
|
|
Bar Code Implemamtation to Production Process of Small Factory
Tihon, Karel ; Špinka, Jiří (referee) ; Starý, Jiří (advisor)
Target of my diploma thesis is barcode study and implementation to SMT assembly processes. This thesis contains two main parts. The first one is devoted to basic types of barcodes, reading technologies and industrial process mapping in PCB assembly. The second part is devoted to theoretical proposal and physical realization of system for materials flow monitoring. Barcode is contained in this system. Practical part of this thesis is tested in a company realizing contract manufacturing in PCB assembly - SMT and THT.
|
|
|
Mini reflow oven
Pavelka, Radek ; Jelínek, Aleš (referee) ; Burian, František (advisor)
This thesis is aimed to design a small oven for PCB soldering using the reflow method. It contains description of the oven’s construction, it’s thermodynamic parameters and the design of the control and power unit PCB as well as their control software. A remote PC control and monitoring application is also a part of this thesis.
|
|
|
Inspection of PCB with SMT by using comparative method
Hejdiš, Roman ; Stejskal, Petr (referee) ; Starý, Jiří (advisor)
The first part of the bachelor´s thesis discuss AOI, types of AOI, its utilization and importance in the industrial production. The second part is devoted to realization of simple comparative inspection method. There were testing effects of ambient light to record photographs of PCB and also artificial light was used. There was problems indication of PCB lit and PCB fixturing. At last, there are discussed some technical problems of this simple comparative method.
|
|
| |
guest ::
