Disertační práce

Model Checking Software

RNDr. Petr Ročkai, učo 139761
Anotace

Systémy které navrhujeme jsou čím dál složitější a je často mimo lidské možnosti ověřit jejich korektnost. Výzkum v oblasti formálních metod vede k implementaci automatických nástrojů, které nám můžou s tímto úkolem pomoct. V současné době se však z různých důvodů užívá formálních metod pouze v ojedinělých případech. Obecným cílem této práce je zlepšit použitelnost metody ověřování modelu v návrhu …více

Abstract

The systems we design are increasing in complexity and it is often beyond human capacity to verify their correctness. Research in formal methods has provided us with automated tools that can help ensure correctness of a system that is beyond our capabilities to check manually. Nowadays, for a variety of reasons, such tools are applied only to a very limited number of systems. The broad goal of this …více

Klíčová slova
Model checking LLVM Explicit-state model checking Software model checking Linear Temporal Logic Parallel algorithms Implementation Multi-threading Shared memory Distributed memory State space reductions Partial order reduction Interpreter Exception handling
Administrativní informace
Práce zkontrolována:
17. 1. 2015 09:02, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
4,3 MB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
9. 6. 2015
Práce byla úspěšně obhájena

Vedoucí

prof. RNDr. Jiří Barnat, Ph.D., učo 3496
KTP FI MU

Oponenti

prof. Ing. Tomáš Vojnar, Ph.D., učo 134390
KPSK FI MU, FIT VUT v Brně
Prof. Dr. Jaco van de Pol
EEMCS, University of Twente
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika (čtyřleté)
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.