|
|
Static Analysis Using Facebook Infer Focused on Performance Analysis
Pavela, Ondřej ; Lengál, Ondřej (referee) ; Rogalewicz, Adam (advisor)
Static analysis has nowadays become one of the most popular ways of catching bugs early in the modern software. However, reasonably precise static analysis tools still often struggle to scale well on large and quickly changing codebases. Efficient static analysers, such as Coverity or Code Sonar, are usually proprietary and difficult to openly evaluate or extend. On the contrary, Facebook Infer offers an open source static analysis framework with the emphasis on compositional, incremental and consequently highly scalable inter-procedural analysis. This thesis presents Looper --- a new performance oriented resource bounds analyser which extends the capabilities of Facebook Infer. We have based our implementation on an existing resource bounds analyser Loopus and evaluated it on two different test suites, showing encouraging results in comparison with the existing Cost analyser developed by the Infer team.
|
|
|
Verification of Pointer Programs Based on Forest Automata
Hruška, Martin ; Rogalewicz, Adam (referee) ; Holík, Lukáš (advisor)
In this work, we focus on improving the forest automata based shape analysis implemented in the Forester tool. This approach represents shapes of the heap using forest automata. Forest automata are based on tree automata and Forester currently has only a simple implementation of tree automata. Our first contribution is replacing this implementation by the general purpose tree automata library VATA, which contains the highly optimized implementations of automata operations. The version of Forester using the VATA library participated in the competition SV-COMP 2015. We further extended the forest automata based verification method with two new techniques - a counterexample analysis and predicate abstraction. The first one allows us to determine whether a found error is a real or spurious one. The results of the counterexample analysis is also used for creating new predicates which are used for the refinement of predicate abstraction. We show that both of these techniques contribute to an improvement over the early approach.
|
|
|
Practical Application of Facebook Infer on Systems Code
Beránek, Tomáš ; Malík, Viktor (referee) ; Vojnar, Tomáš (advisor)
Statická analýza je dnes často využívána ve vývojovém procesu pro hledání defektů v produkovaném softwaru. I když nástroje na statickou analýzu dokáží hledat defekty v softwarech o miliónech řádků kódu, mají také řadu nevýhod. Hlavními nevýhodami jsou náročnost nasazení nástroj na vyvíjený projekt, vysoký počet falešných hlášení a časové i paměťové požadavky. Tato práce se zaměřuje na zmírnění těchto negativních vlastností u nástroje Facebook Infer, zejména pro analýzu Linuxových nástrojů v podobě SRPM balíčků. Pro zjednodušení nasazení byl vytvořen modul pro nástroj csmock, který umožňuje automaticky spouštět statické analyzátory nad balíčky pro CentOS a Fedoru. Pro snížení počtu falešných hlášení byl vytvořen filtr, který filtruje výstup Inferu podle heuristik, které byly navrženy na základě zkušeností získaných kontrolou hlášení z Inferu. Filtr byl také zapojen do modulu pro csmock a otestován na řadě balíčků. Na analyzovaných balíčcích filtr dokázal odstranit 60 % falešných hlášení se ztrátou 2.5 % skutečných defektů. Doba potřebná pro běh analýzy může být zkrácena použitím inkrementální analýzy. U inkrementální analýzy Inferu byly experimentálně zjištěny nedostatky, proto se tato práce věnuje také vytvoření nástavby nad Inferem, která nahrazuje inkrementální analýzu v Inferu.
|
|
|
Static Analysis in the Frama-C Environment Focused on Deadlock Detection
Dacík, Tomáš ; Holík, Lukáš (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá návrhem nového statického analyzátoru pro detekci uváznutí, implementovaného jako plugin platformy Frama-C. Kromě samotného algoritmu pro detekci uváznutí představuje také odlehčené řešení, které umožňuje využít platformu Frama-C pro analýzu vícevláknových programů s využitím analyzátorů Frama-C podporujících pouze sekvenční programy. Výsledky experimentů ukazují, že implementovaný nástroj je schopný analyzovat reálné programy s vysokou přesností. Pro demonstraci další rozšiřitelnosti je představeno experimentální rozšíření umožňující detekovat také časově závislé chyby nad daty.
|
|
|
Administration Building
Luža, Radim ; Šulák, Pavel (referee) ; Jeneš, Rostislav (advisor)
This bachelor’s thesis deals with the static analysis and assessment of reinforced concrete floor slab above the first ground floor of the administrative building. The ceiling structure consists of a monolithic floor slab, locally supported. The Static analysis was carried out using a programme called Scia Engineer 14. The verification of the calculation was done by the same software, but with two perpendicular frames instead of a modeled plate. Subsequently, we could define the limit state of the dimensioning capacity. The investigation of the ultimate limit state was mainly about bending moments and embossing. Further to It was also carried out assessment of the second limit state, so usability. The second limit state investigations was mainly about limitation of cracks. The drawing documentation was based on the static analysis and advice to single limit states, including a lower and upper reinforcer and extrusion.
|
|
|
Dynamic analysis of steel tank with liquid
Farkasová, Zuzana ; Mrózek, Michal (referee) ; Hradil, Petr (advisor)
Master´s thesis deals with dynamic analysis of steel tank with liquid. There are given parametres of structure and thein introduction to ANSYS system. There are created three numerical models for comparison, which are static and modal analysis calculated for. Spectrum analysis is calculated only for numerical models with fluid elements. Shell elements are evaluated according to EC 3.
|
|
| |
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (referee) ; Radu, Iosif (referee) ; Vojnar, Tomáš (advisor)
Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.
|
|
|
Using optimization methods to design machine parts
Kubrický, Daniel ; Pokorný, Přemysl (referee) ; Zeizinger, Lukáš (advisor)
This bachelor thesis describes using structural optimization methods to design machine parts. In the first part of the thesis, a description of the current state of knowledge of the optimization process was made together with its theoretical background. In the second part of the thesis, a static analysis and topology optimization or Generative design was developed using the example of a bell crank in six commercial software. In the third part, the resulting models of each software were compared with each other, and the results were compared using the von Mises maximum stress criterion and the overall model deformation. Finally, this work was concluded with an evaluation of the use of the structural optimization software.
|
|
|
Statická analýza v nástroji Meta Infer zaměřená na detekci souběhu nad daty
Svobodová, Lucie ; Fiedor, Jan (referee) ; Vojnar, Tomáš (advisor)
Vícevláknové programy jsou v moderních softwarových systémech využívány ke zlepšení výkonu a zvýšení efektivity. Zajištění spolehlivosti a bezpečnosti takových programů však může být náročné kvůli zvýšenému množství chyb, které se v nich vyskytují, včetně souběhu nad daty. V této práci představujeme nový statický detektor souběhu nad daty, DarC, navržený k analýze programů napsaných v jazyce C využívajících knihovnu Pthreads. Navrhovaný nástroj byl implementován jako zásuvný modul prostředí Meta Infer, což je nástroj pro statickou analýzu programů, který klade důraz na kompoziční, inkrementální a díky tomu i vysoce škálující analýzu programů. Nový analyzátor zaznamenává množinu přístupů ke sdíleným proměnným, ke kterým v analyzovaném programu došlo, spolu s informací o množině zámků uzamknutých při jednotlivých přístupech. Množina přístupů je dále použita k identifikaci dvojic přístupů, mezi nimiž by k souběhu nad daty mohlo dojít. Nástroj byl úspěšně ověřen na sadě testovacích vícevláknových programů, stejně tak jako na několika programech běžně využívaných v praxi, čímž byl ukázán jeho potenciál pro efektivní detekci souběhu nad daty v programech napsaných v programovacím jazyce C.
|
guest ::
