|
|
Využití formálních metod v přibližném počítání
Matyáš, Jiří ; Kubátová, Hana (oponent) ; Kumar, Akash (oponent) ; Pozzi, Laura (oponent) ; Češka, Milan (vedoucí práce)
V minulosti se výkon počítačových systémů zvyšoval hlavně díky tzv. Mooreovu zákonu - každé dva roky se počet transistorů na čipu přibližně zdvojnásobí. V současné době tento zákon přestává platit a tak se objevují a vyvíjí nové alternativní výpočetní přístupy, které mají za úkol zrychlit a zefektivnit výpočetní systémy. Jedním z těchto přístupů je tzv. aproximované počítání, které se snaží urychlit a zefektivnit výpočty za cenu přijatelných nepřesností ve výsledcích. Tento přístup je aplikovatelný hlavně v oblastech, které jsou přirozeně odolné vůči chybám - např. neuronové sítě nebo zpracování multimédií. Techniky pro aproximované počítání se postupně vyvinuly na všech úrovních výpočetních systémů. V rámci této práce se zaměřujeme na prohledávací algoritmy pro přibližný návrh hardwarových aritmetických obvodů. Aproximace aritmetických obvodů má velký potenciál, protože tyto obvody slouží jako základní stavební kameny větších systémů. Automatizované prohledávací aproximační algoritmy často pracují iterativně. V každé iteraci se nejprve vytvoří kandidátní aproximovaná řešení (pomocí komponenty zvané syntetizér), a poté se vyhodnotí jejich chyba vzhledem ke správnému řešení (komponenta analyzátor). Pro získání kvalitních aproximovaných obvodů musí prohledávací algoritmy vykonat velké množství těchto iterací. Proto je nutná vysoká efektivita syntetizéru i analyzátoru. Abychom zvýšili výkonnost těchto komponent, zapojujeme do prohledávacího algoritmu založeném na Kartézském genetickém programování (CGP) metody formální verifikace. Analyzátor je akcelerován za použití speciálního obvodu zvaného aproximační miter, který nám umožňuje převést vyhodnocení chyby obvodu na rozhodovací problém a tento problém vyřešit pomocí nástrojů zvaných SAT solvery. Další zrychlení aproximačního algoritmu přináší nově navržená strategie, která uvaluje limit na prostředky, které může SAT solver využít při vyhodnocování chyby kandidátních řešení. Díky tomuto limitu je evoluční algoritmus motivován hledat rychle verifikovatelná řešení. Výsledkem je větší množství iterací prohledávacího algoritmu a tím pádem také vyšší kvalita výsledných aproximovaných obvodů. Použitý evoluční algoritmus se může během aproximace "zaseknout" v tzv. lokálních optimech. Navržené vylepšení syntetizéru integruje CGP a optimalizaci pod-obvodů využívající SAT solver umožňuje evolučnímu algoritmu uniknout z lokálních optim. Díky tomu může algoritmus dále zlepšovat řešení i v případech, v nichž by se původní varianta CGP již dále nezlepšila. Dalším navrženým vylepšením syntetizéru je nový mutační operátor pro CGP, vytvořený speciálně pro co nejefektivnější aproximaci obvodů. Výsledky prezentované v rámci této dizertační práce výrazně vylepšují výkonnost prohledávacích algoritmů pro aproximaci aritmetických obvodů. Díky tomu můžeme získat aproximace obvodů velkých bitových šířek se složitou vnitřní strukturou (např. 32bitové násobičky nebo 128bitové sčítačky), které poskytují doposud nejlepší známý poměr mezi aproximační chybou a spotřebou elektrické energie.
|
|
|
Static Analysis of C Programs
Malík, Viktor ; Zuleger, Florian (oponent) ; Strejček, Jan (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis proposes several original contributions to the area of static analysis of software with focus on low-level systems code written in C. The contributions are split into two parts, each related to a different area of static analysis, namely formal verification of (low-level) C code and static analysis of semantic equivalence of different versions of the same software. The first part proposes new analyses suitable for verification engines that perform automatic invariant inference using an SMT solver. The proposed solution includes two abstract template domains that use logical formulae over bit-vectors to encode the shape of the program heap and the contents of the program arrays. The shape domain is based on computing a points-to relation between pointers and symbolic addresses of abstract memory objects. The array domain is based on splitting the arrays into several non-overlapping contiguous segments and computing a different invariant for each of them. Both domains can be combined with value domains in a straightforward manner, which particularly allows our approach to reason about shapes and contents of heap and array structures at the same time. The information obtained from the analyses can be used to prove memory safety and reachability properties, expressed by user assertions, of programs manipulating data structures. All of the proposed solutions have been implemented in the 2LS framework and compared against state-of-the-art tools that perform the best in the relevant categories of the well-known Software Verification Competition (SV-COMP). Results show that 2LS outperforms these tools on benchmarks requiring combined reasoning about unbounded data structures and their numerical contents. The second part of the thesis is motivated by existence of software projects that undergo regular refactorings and modifications and yet need to ensure semantic stability of some of their core parts. This part proposes a highly-scalable approach for automatically checking semantic equivalence of different versions of large, real-world C projects, with a particular focus on the Linux kernel. The proposed method uses a novel combination of pattern matching with light-weight static analysis and control-flow transformations. The method checks preservation of the semantics of functions forming the API of the project being analyzed as well as of the semantics of its global variables, which typically hold various control parameters. For the latter, a specialised slicing procedure is proposed to slice out code influenced by these variables and concentrate the further analysis on that code only. Although the method cannot prove equivalence on heavily refactored code, it can compare thousands of functions in the order of minutes while producing a low number of false non-equality verdicts as our experiments show. The method has been implemented over the LLVM infrastructure in a tool called DiffKemp. Our results show that DiffKemp, unlike other existing tools, gives practically useful results even on projects of the size of the Linux kernel.
|
|
|
Automata in Software Verification and Testing
Hruška, Martin ; Rezine, Ahmed (oponent) ; Kofroň, Jan (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis focuses on applications of automata theory to software quality. In the first part, we focus on shape analysis which can be used for formal verification of programs manipulating dynamic data structures. Particularly, we develop an approach of backward program execution along possible counterexamples tracesvand counterexample-guided refinement for shape analysis based on forest automata. We also introduce a new approach based on automata over graphs with a bounded tree width which is more general than forest automata but still has feasible computation properties. In the second part, we introduce a method for automated testing of manufacturing execution systems (MES) in digital twin. We are able to orchestrate a digital twin to reproduce behaviour of a real-world setting in which MES is deployed and so provide a safe environment for testing. Moreover, we can generate new test cases by applying automata and abstraction over them in this context.
|
|
|
Statistické ověřování modelů přibližných výpočetních systémů
Blažek, Michal ; Sekanina, Lukáš (oponent) ; Strnadel, Josef (vedoucí práce)
Tato bakalářská práce se zaměřuje na statistické ověřování modelů přibližných násobiček. Zejména se zabývá srovnáním vlastností násobiček při generování jejich vstupních hodnot podle různých pravděpodobnostních rozdělení. Součástí práce je převod modelů násobiček z knihovny EvoApproxLib do modelů v prostředí UPPAAL. Vytvořené modely jsou poté simulovány s ohledem na vybrané hodnotící metriky, jako např. pravděpodobnost chyby, průměrná absolutní chyba aj. Ze získaných výsledků lze usuzovat, že použitím vhodné aproximační násobičky pro provádění výpočtů v rámci konkrétní aplikace je možné docílit menší chyby ve výpočtech. Výsledky by proto mohly mít další uplatnění v oblasti přibližných výpočetních systémů.
|
|
|
HyperLTL Model Checking
Alexaj, Ondrej ; Strejček, Jan (oponent) ; Lengál, Ondřej (vedoucí práce)
HyperLTL model checking is an approach to verifying a system against a given hyperproperty, which is able to relate multiple executions of a system. The algorithmic approach based on automata which relies on standard -automata operations is well established. The aim of this work is to outperform the complete state-of-the-art HyperLTL model checker AutoHyper by employing more efficient partial automata operations, in particular complementation and inclusion. The implementation of HyperLTL model checking in a novel modular-based complementation tool Kofola resulted in a significant enhancement in performance compared to the reference tool. Finally, our approach to language inclusion checking shows a notable improvement in terms of the generated state space. As a commonly used automata operation, it could potentially contribute to the advancement of other areas of verification.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (oponent) ; Veith, Helmut (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
The work presented in this thesis focuses on finite state automata over finite words and finite trees, and the use of such automata in formal verification of infinite-state systems. First, we focus on extensions of a previously introduced framework for verifi cation of heap-manipulating programs-in particular programs with complex dynamic data structures-based on tree automata. We propose several extensions to the framework, such as making it fully automated or extending it to consider ordering over data values. Further, we also propose novel decision procedures for two logics that are often used in formal verification: separation logic and weak monadic second order logic of one successor. These decision procedures are based on a translation of the problem into the domain of automata and subsequent manipulation in the target domain. Finally, we have also developed new approaches for efficient manipulation with tree automata, mainly for testing language inclusion and for handling automata with large alphabets, and implemented them in a library for general use. The developed algorithms are used as the key technology to make the above mentioned techniques feasible in practice.
|
|
|
Nástroj pro statickou analýzu programů se seznamy
Kotoun, Michal ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tvorba softwarového analyzátoru je komplexní úloha -- je nutno implementovat parsování zdrojového kódu, reprezentaci instrukcí, abstrakci hodnot, uživatelské rozhraní, ... a také analýzu samu. Abychom předešli zbytečné práci vývojářů analýz, rozhodli jsme se vytvořit framework pro statickou analýzu programů. Předkládáme obecný návrh frameworku zvaného Angie s důrazem na jeho použitelnost a popisujeme prototyp frameworku, včetně modelové analýzy založené na symbolických paměťových grafech. Angie je implementován v C++ a používá nástroje z kolekce LLVM pro parsování zdrojového kódu analyzovaných programů.
|
|
|
Efektivní algoritmy pro práci s konečnými automaty
Hruška, Martin ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Nedeterministické konečné automaty jsou používány v mnoha oblastech informatiky, mimo jiné také ve formální verifikaci, při návrhu číslicových obvodů nebo pro reprezentaci regulárlních jazyků. Jejich výhodou oproti deterministickým konečným automatům je schopnost až exponenciálně stručnější reprezentace jazyka. Nicméně, tato výhoda může být pozbyta, jestliže je zvolen naivní přístup k implementaci některých operací, jako je na\-pří\-klad test jazykové inkluze dvojice automatů, jehož naivní implementace provádí explicitní determinizaci jednoho z automatů. V nedávné době bylo ale představeno několik nových přístupů, které právě explicitní determinizaci při testu jazykové inkluze předcházejí. Tyto přístupy využívají tzv. antichainů nebo tzv. bisimulace vzhůru ke kongruenci. Cílém této práce je vytvoření efektivní implementace zmíněných přístupů v podobě nového rozšíření knihovny VATA. Vytvořená implementace byla otestována a je až řádově rychlejší v 90% testovaných případů nežli implementace jiné
|
|
|
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.
|
|
|
Dynamická detekce a léčení časově závislých chyb nad daty v prostředí Java
Letko, Zdeněk ; Kolář, Dušan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Hledání chyb plynoucích ze souběžného zpracovávání výpočtů je obtížné. Proto se tato diplomová práce zabývá detekcí a léčením časově závislých chyb nad daty a chyb plynoucích z nesprávné atomicity operací v prostředí Java. Práce prezentuje dva různé algoritmy pro detekci. Jedním z nich je nový algoritmus nazvaný AtomRace, který detekuje časově závislé chyby nad daty jako speciální případ nesprávné atomicity operací. Následné léčení detekovaných chyb je založeno na potlačení opakování chyby, buď zavedením přídavné synchronizace, nebo legálním ovlivňováním plánovače Javy, za účelem vynucení správné atomicity operací. Navržená architektura, která pracuje souběžně se sledovaným programem, využívá ke sledování a ovlivňování výpočtu techniku instrumentace na úrovni Java bytecode. Architektura a algoritmy byly implementovány a otestovány v několika případových studiích.
|
host ::
RSS.