|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
The goal of this work is to propose a shape analysis suitable for the context of the 2LS analyser. 2LS is a program analysis framework for C programs which is based on automatic invariant inference using an SMT solver. The proposed solution includes a way how the shape of a program heap can be described using logical formulae over bit-vectors and how a first-order SMT solver can be used to infer loop invariants and function summaries for each function of the analysed program. Our approach is based on pointer access paths that describe the shape of the heap by expressing the reachability of heap objects from pointer-typed program variables. The information obtained from the analysis can be used to prove various properties of programs manipulating dynamic data structures, mainly linked lists. The solution has been implemented in the 2LS framework and it brought a significant improvement in terms of the capabilities of 2LS in analysing heap-manipulating programs. This is demonstrated on benchmarks taken from the well-known International Competition on Software Verification (SV-COMP) as well as other benchmarks.
|
|
|
String Analysis for Code Contracts
Dort, Vlastimil ; Parízek, Pavel (vedoucí práce) ; Kofroň, Jan (oponent)
Jedním ze způsobů prevence chyb v objektově orientovaných programech je používání kontraktů, kterými jsou například vstupní a výstupní podmínky metod nebo invarianty tříd. Ve frameworku .NET je používání kontraktů umožněno díky frameworku Code Contracts, který mimo jiné obsahuje nástroj Clousot na statickou analýzu programů, založený na abstraktní interpretaci. Ačkoli řetězce jsou jedním ze základních typů v programech pro .NET, Clousot neobsahuje použitelnou podporu pro analýzu řetězcových hodnot. V této práci probereme specifika práce s řetězci v jazyce C# a frameworku .NET a ukážeme, jak je možné ji pokrýt statickou analýzou. Zvolený přístup využívá metody třídy String a omezenou podmnožinu regulárních výrazů ke specifikaci vlastností řetězců v kódu, a abstraktní interpretaci s nerelačními abstraktními doménami k důkazům těchto vlastností. Zvolili jsme několik již publikovaných abstraktních domén pro řetězce, které se mezi sebou liší složitostí a schopností reprezentovat různé vlastnosti řetězců. Tyto domény jsme adaptovali pro zvolené prostředí, což zahrnovalo definici abstraktní sémantiky pro podporované řetězcové operace. Abstraktní domény jsme implementovali v nástroji Clousot, a to tak, aby bylo v budoucnu možné rozšíření o další domény. Powered by TCPDF (www.tcpdf.org)
|
|
|
Analýza práce s dynamickými datovými strukturami v C programech
Šoková, Veronika ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Táto diplomová práca sa zaoberá analýzou dynamických dátových štruktúr pomocou analýzy tvaru použitej v nástroji Predator. Popisuje zvolenú abstraktnú doménu pre reprezentáciu pamäte vo forme symbolických grafov pamäte. Ďalej sa zaoberá návrhom prostredia pre vývoj statických analyzátorov nad clang/LLVM. Prínosom tejto práce je vytvorenie a otestovanie transformačných priechodov zjednodušujúcich LLVM IR medzikód. Ďalším prínosom je optimalizácia parametrov paralelnej nadstavby Predatora opakovaným spúšťaním testov z medzinárodnej súťaže SV-COMP'16, kde táto verzia nástroja Predator získala zlatú medailu v kategórii Heap Data Structures. Posledným prínosom je návrh architektúry samotného verifikačného jadra s ohľadom na SMG doménu.
|
|
|
Statická analýza možných hodnot proměnných v programech v C
Ďuričeková, Daniela ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
Analýza rozsahu hodnot (anglicky value-range analysis) je metoda statické analýzy založená na zjišťování hodnot, kterých může daná proměnná nabývat v určitém místě v programu. Tato technika může být použita k dokázání, že se v programu nevyskytují chyby za běhu, jako například přístup za hranici pole. Jelikož analýza rozsahu hodnot získává informace o každém místě v programu, lze k její implementaci využít analýzu toku dat (anglicky data-flow analysis). Cílem této diplomové práce je návrh a implementace funkčního nástroje provádějícího analýzu rozsahu hodnot. Práce začíná úvodem do problematiky, vysvětlením analýz toku dat a hodnot proměnných a popisem abstraktní interpretace, která tvoří formální základ analyzátoru. Následuje seznámení s prostředím Code Listener, které bylo využito k implementaci analyzátoru. Jádro práce tvoří návrh, implementace a otestování analyzátoru. V závěru jsou shrnuty nabyté zkušenosti a diskutovány možnosti budoucího vývoje vytvořeného nástroje.
|
host ::
RSS.