|
|
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.
|
|
| |
|
|
A Decision Procedure for Strong-Separation Logic
Dacík, Tomáš ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Separation logic (SL) is one of the most successful tools for verification of programs that manipulate dynamically allocated memory. Its expressive power, however, comes at a cost of undecidability when several of its features are combined, especially separating implications. To circumvent this problem, the recently introduced strong-separation logic (SSL) uses a stricter definition of the semantics, making it decidable, while remaining suitable for verification. However, there is currently no implementation of a decision procedure for SSL. In this work, we propose a decision procedure for SSL based on a translation to first-order formulae that can be later solved by a specialised solver. Our experimental results on restricted fragments where SL and SSL coincide show that our approach can effectively solve formulae obtained from verification tools based on SL and also outperform all other existing translation-based decision procedures. Moreover, during our experiments, we found cases of unsoundness of the heuristics implemented in the decision procedure for SL that is a part of the well-known cvc5 SMT solver. Based on our reports, those heuristics has been fixed.
|
|
|
A Decision Procedure for Strong-Separation Logic
Dacík, Tomáš ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Separation logic (SL) is one of the most successful tools for verification of programs that manipulate dynamically allocated memory. Its expressive power, however, comes at a cost of undecidability when several of its features are combined, especially separating implications. To circumvent this problem, the recently introduced strong-separation logic (SSL) uses a stricter definition of the semantics, making it decidable, while remaining suitable for verification. However, there is currently no implementation of a decision procedure for SSL. In this work, we propose a decision procedure for SSL based on a translation to first-order formulae that can be later solved by a specialised solver. Our experimental results on restricted fragments where SL and SSL coincide show that our approach can effectively solve formulae obtained from verification tools based on SL and also outperform all other existing translation-based decision procedures. Moreover, during our experiments, we found cases of unsoundness of the heuristics implemented in the decision procedure for SL that is a part of the well-known cvc5 SMT solver. Based on our reports, those heuristics has been fixed.
|
|
|
STP řešič pro OpenSMT
Luňák, Václav ; Kofroň, Jan (vedoucí práce) ; Kučera, Petr (oponent)
Simple Temporal Problem je jedním z nejdůležitějších plánovacích problémů. V kontextu formální verifikace úzce souvisí s problémem SMT, kde na něj narazíme při řešení teorie dife- renční logiky. V této práci se věnujeme doplnění řešiče pro diferenční logiku do vyvíjejícího se SMT řešiče OpenSMT. Zkoumáme existující postupy pro řešení problému a porovnáváme je s ohledem na možnost jejich využití v kontextu OpenSMT. Detailně rozebíráme algoritmus založený na vyčerpávající propagaci teorie a na jeho bázi navrhujeme a vytváříme efektivní im- plementaci řešiče. Tuto implementaci následně testujeme a srovnáváme s ostatními současnými SMT řešiči a ukazujeme tak její srovnatelnou výkonnost. 1
|
host ::
RSS.