Diplomová práce

Verification of Memory Safety with Predator and Symbiotic

Bc. Tomáš Jašek
Anotace

Symbiotic a Predator sú nástroje na formálnu verifikáciu. Každý nástroj vyhodnotíme na benchmarkoch zo súťaže sv-comp. Naše výsledky ukazujú, že nástroje by mohli spoločne dosiahnuť lepšie výsledky. Aby mohli spolupracovať, vyladíme výkon nástroja Predator na programoch v llvm. Následne popíšeme integráciu týchto dvoch nástrojov. Integrácia číta vstup nástroja Predator a používa jeho výsledky v Symbioticu …více

Abstract

Symbiotic and Predator are formal verification tools. We evaluate each of those tools on benchmarks from sv-comp. Our evaluation shows that the tools can benefit from cooperating. To enable cooperation, we tune Predator to run on llvm. Then, we describe an integration of these two tools. The integration parses output of Predator and uses the result in Symbiotic instrumentation component to mark potentially …více

Klíčová slova
formal methods Formela program analysis software analytics software reliability static code analysis Symbiotic verification
Zadání práce
Cílem práce je vyladit výkon nástroje Symbiotic při verifikaci bezpečné práce s pamětí. Student nedávno upravil nástroj Symbiotic tak, aby používal výsledky nástroje Predator. Nástroj Symbiotic analyzuje programy přeložené do LLVM. Bohužel se ukázalo, že Predator nad těmito programy nedosahuje tak dobrých výsledků jako při analýze originálních programů v C. Hlavním úkolem je tedy vyladit výkon nástroje Predator nad LLVM programy a dále popsat integraci nástroje Predator do nástroje Symbiotic. Výsledky budou doloženy experimentálním srovnáním původních a výsledných verzí nástrojů Predator a Symbiotic.
Administrativní informace
Práce zkontrolována:
8. 1. 2021 09:54, prof. RNDr. Jan Strejček, Ph.D., učo 3366
Plný text práce
586,4 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
8. 2. 2021
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jan Strejček, Ph.D., učo 3366
KTP FI MU

Oponent

RNDr. Vladimír Štill, Ph.D., učo 373979
KPSK FI MU

Konzultant

RNDr. Marek Chalupa, Ph.D.
KTP FI MU

Literatura

  • CHALUPA, Marek; Tomáš JAŠEK; Lukáš TOMOVIČ; Martin HRUŠKA; Veronika ŠOKOVÁ; Paulína AYAZIOVÁ; Jan STREJČEK a Tomáš VOJNAR. Symbiotic 7: Integration of Predator and More (Competition Contribution). In Armin Biere, David Parker. Tools and Algorithms for the Construction and Analysis of Systems. Německo: Springer, 2020, s. 413-417. ISBN 978-3-030-45236-0. Dostupné z: https://doi.org/10.1007/978-3-030-45237-7_31.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.