Rigorózní práce

Model Checking Software

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

Systémy které navrhujeme se stávají složitějšími a ověřit jejich správnost je často mimo lidských možností. Máme ovšem k dispozici formální metody, díky kterým lze ověřovat správnost systémů, které by jinak byly zcela mimo dosah ručních metod. V současnosti, z mnoha různých důvodů, jsou formální metody aplikovány jen v omezeném počtu případů. Širším cílem navrhované disertace je zlepšit aplikovatelnost …více

Abstract

The systems we design are increasing in complexity, and it is often beyond human capacity to verify their correctness. Formal methods exist to augment the human verifier with automated tools that can help them ensure correctness of a system that would be far beyond their capabilities to check manually. Nowadays, for a variety of reasons, formal methods are applied only to a very limited number of …více

Klíčová slova
Model checking Low-Level Virtual Machine 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
Administrativní informace
Práce zkontrolována:
9. 11. 2011 07:34, prof. RNDr. Luboš Brim, CSc.
Plný text práce
358,8 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
11. 1. 2012
Práce byla úspěšně obhájena

Oponenti

doc. Mgr. Radek Pelánek, Ph.D., učo 4297
KSUZD FI MU
RNDr. Ondřej Šerý, Ph.D.
MFF UK v Praze
Autor posudku dosud neidentifikován.
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.