Diplomová práce

Predicate Abstraction of DiVinE Models

Bc. Jiří Novosad, učo 99288
Anotace

Cílem diplomové práce je prozkoumat možnost realizace verifikačního schématu CEGAR (Counterexample Guided Abstraction Refinement) v kontextu použití verifikačního nástroje DiVinE. Práce dostatečně podrobně popíše celé schéma verifikační metody CEGAR a identifikuje možná obtížná místa realizace. Práce se dále zaměří na realizaci predikátové abstrakce DiVinE modelů pro danou vstupní množinu predikátů.

Abstract

The aim of this thesis is to explore the possibility of implementing the CEGAR (Counterexample Guided Abstraction Refinement) verification schema in the context of the DiVinE verification tool. The thesis will describe the full schema of the CEGAR verification method in sufficient detail and identify potential difficult points of an implementation. Further, the thesis will focus on implementing predicate abstraction of DiVinE models for a given set of predicates.

Klíčová slova
DiVinE DVE model checking predicate abstraction counterexample guided abstraction refinement LTL
Zadání práce
The aim of this thesis is to explore the possibility of implementing the CEGAR (Counterexample Guided Abstraction Refinement) verification schema in the context of the DiVinE verification tool. The thesis will describe the full schema of the CEGAR verification method in sufficient detail and identify potential difficult points of an implementation. Further, the thesis will focus on implementing predicate abstraction of DiVinE models for a given set of predicates.
Administrativní informace
Práce zkontrolována:
4. 6. 2012 11:58, prof. RNDr. Jiří Barnat, Ph.D., učo 3496
Plný text práce
601,1 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
26. 6. 2012
Práce byla úspěšně obhájena

Vedoucí

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

Oponent

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

Literatura

  • GRUMBERG, Orna; Doron A. PELED a E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708.
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
 
Název
Vložil
Vloženo
Práva
Archiv závěrečné práce Jiří Novosad FI N-IN PDS, učo 99288 qpaxh/7
Dvořáková, A.
23. 4. 2012
Složky
Soubory
Anotace anglicky annotation_english.txt
Novosad, J.
27. 5. 2012
Anotace česky annotation.txt
Novosad, J.
27. 5. 2012
Klíčová slova keywords.txt
Novosad, J.
27. 5. 2012
Plný text práce thesis.pdf
Novosad, J.
27. 5. 2012
Posudek oponenta posudek_novosad2012.pdf
Strejček, J.
19. 6. 2012
Příloha abstract-dve.tar.gz
Novosad, J.
27. 5. 2012

  • 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.