|
|
Heuristics in String Solving
Řezáč, Michal ; Havlena, Vojtěch (oponent) ; Síč, Juraj (vedoucí práce)
This work aims on identifying heuristics and strategies used in modern string solvers and evaluating their impact on the effectiveness of the solving. In particular, two solvers -- cvc5 and Z3 -- are examined. The thesis describes the techniques used by SMT solvers and the strategies implemented by string solvers. The evaluation of the effectiveness of the heuristics was performed by disabling them directly in the code of the tools mentioned and then evaluating the impact on solving the sets of standard benchmarks. The result of this work is summary of a set of specific heuristics and a description of the structure of the tools cvc5 and Z3. The measurements failed to demonstrate the actual impact of the heuristics identified and described.
|
|
|
Transducers in Automata Library Mata
Chocholatý, David ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
We implement finite transducers in a new fast and simple automata library Mata. Finite transducers are finite state machines modelling rational relations. Our primary use case for finite transducers is encoding replace operations (replacing a word or a regular pattern with a string literal). A recent automata-based SMT string solver Z3-Noodler uses Mata as a backbone of its decision procedure. Z3-Noodler needs finite transducers to analyse string manipulating programs with replace operations. The analysis of said programs used in web applications prevents software attacks such as cross-site scripting (XSS) or code injection. The distinctive features of Mata include simplicity (simple to use, modify and extend) and efficiency (fast to run). We design the representation and algorithms for finite transducers to fit the simplicity and efficiency requirements. We inherit and extend the existing data structures and algorithms for finite automata in Mata to represent the finite transducers and their operations. The representation for finite transducers serves as a common data structure and interface for the finite transducers and future representation of automata using multi-terminal binary decision diagrams to handle large alphabets. We further extend the design with algorithms to construct finite transducers modelling replace operations defined in SMT-LIB. Finally, we run an experimental evaluation of performance of finite transducers in Mata on a new benchmark with replace operations from runs of Z3-Noodler and from solving problems in pattern matching.
|
|
|
Modernizace osazovacího automatu Tenryu
Drška, Jan ; Szabó, Zoltán (oponent) ; Mikulka, Jan (vedoucí práce)
Cílem diplomové práce je zhodnotit stávající stav osazovacího automatu a navrhnout možné řešení modernizace stroje a realizovat vybrané části. Součástí práce je dokumentace původního stavu automatu Tenryu MT-5530LQ a jeho dokumentace po modernizaci. V úvodní části je popsána teorie osazovacích automatů, na tuto kapitolu navazuje popis funkce a konstrukce již zmíněného automatu. Ve třetí kapitole se nacházejí popsané a vytipované součásti stroje, které je nutno nahradit, či opravit. Ve čtvrté kapitole této práce se nachází kompletní návrh modernizace automatu včetně možných výsledků modernizace. Na tyto předchozí kapitoly navazují kapitoly číslo 5, 6 a 7, kde jsou popsané nové karty pro nový řídicí systém a práce je zakončena shrnutím dopadu modernizace na stroj včetně možností dalšího pokračování na modernizaci stroje.
|
|
|
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.
|
|
|
Opravy DPS s BGA a FC pouzdry
Buřival, Tomáš ; Špinka, Jiří (oponent) ; Starý, Jiří (vedoucí práce)
Práce je zaměřena na problematiku pouzder integrovaných obvodů s kuličkovými vývody. Kapitola druhá popisuje jednotlivé typy těchto pouzder a srovnání jejich vlastností. Dále se v kapitole třetí práce zabývá možnostmi oprav desek osazených těmito pouzdry, montáží a demontáží pouzder, metodou kamerového sesouhlasení a také možnostmi kontroly provedeného pájení. Čtvrtá kapitola je věnována praktickému měření teplotních profilů, jejich optimalizaci.
|
|
|
Verifikovaná knihovna datových struktur
Rychnovský, Jan ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá metodikou psaní verifikovaných programů pomocí nástroje VCC. Zmíněná metodika je založena na principu doplnění kódu programu o anotace, jež poskytují specifikaci požadované funkcionality. Nástroj VCC pak prostřednictvím formálních metod určí zda zdrojový kód splňuje danou specifikaci či ne. V první části práce je popsána formální verifikace a zmíněny tři základní přístupy k ní. Následně jsou popsány problémy splnitelnosti výrokových formulí (SAT) a splnitelnosti formulí v teoriích predikátové logiky (SMT). Práce se dále věnuje popisu verifikačního nástroje VCC, jeho funkčnosti, metodice, syntaxi a sémantice příkazů jeho anotačního jazyka BoogiePL. Druhá část textu je zaměřena na popis návrhu a implementace verifikované knihovny datových struktur obsahující jednosměrný, dvousměrný a kruhový seznam, binární vyhledávací strom a Treiberův zásobník. Závěr práce diskutuje získané poznatky o programovací metodice založené na psaní verifikovaného kódu.
|
|
|
Implementace čárového kódu do výrobního procesu malé firmy
Tihon, Karel ; Špinka, Jiří (oponent) ; Starý, Jiří (vedoucí práce)
Cílem mojí diplomové práce je studium a implementace čárového kódu do SMT montážního procesu. Tato práce se skládá ze dnou hlavních částí. První pojednává o typech čárových kódů, technologiích čtení a mapuje výrobní proces ve firmě zabývající se montáží PCB. Druhá část je tvořena teoretickým návrhem a fyzickou realizací monitorovacího systému pro kontrolu materiálového toku. Čárový kód je implementován do tohoto systému. Praktická část této práce je testována ve firmě zabývající se zakázkovou výrobou PCB – SMT a THT.
|
|
|
Malá pec pro reflow
Pavelka, Radek ; Jelínek, Aleš (oponent) ; Burian, František (vedoucí práce)
Tato práce se zabývá návrhem prototypu malé pece pro pájení plošných spojů pomocí metody reflow. Je zde popsána konstrukce pece, její termodynamické vlastnosti a návrh řídící a výkonové elektroniky a softwaru ji ovládajícího. Součástí návrhu je i obslužná aplikace pro vzdálené nastavení a kontrolu průběhu ohřevu z PC.
|
|
|
Inspection of PCB with SMT by using comparative method
Hejdiš, Roman ; Stejskal, Petr (oponent) ; Starý, Jiří (vedoucí práce)
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.
|
|
| |
host ::
RSS.