Master's thesis

Predicate Abstraction of DiVinE Models

Bc. Jiří Novosad, UČO 99288
Abstract

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.

Keywords
DiVinE DVE model checking predicate abstraction counterexample guided abstraction refinement LTL
Thesis description
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.
Administrative information
The thesis has been checked:
4/6/2012 11:58, prof. RNDr. Jiří Barnat, Ph.D., UČO 3496
Full text of thesis
601,1 KB / file PDF
Attachments (1)
Language used
English English
Defence date
26/6/2012
The thesis was defended successfully

Supervisor

prof. RNDr. Jiří Barnat, Ph.D., UČO 3496
KTP FI MU

Reader

prof. RNDr. Jan Strejček, Ph.D., UČO 3366
KTP FI MU

Literature

  • GRUMBERG, Orna; Doron A. PELED and E. M. CLARKE. Model checking. Cambridge: MIT Press, 1999, xiv, 314. ISBN 0262032708.
Cite this text
Masaryk University Faculty of Informatics
Programme
Informatics
Field of Study

Theses on a related topic

List of theses with an identical keyword.

Similar documents
 
Name
Posted by
Uploaded/Created
Rights
Archive of Thesis/Dissertation Jiří Novosad FI N-IN PDS, učo 99288 qpaxh/7
Dvořáková, A.
23/4/2012
Folders
Files
Abstract (in English) annotation_english.txt
Novosad, J.
27/5/2012
Abstract (in Czech) annotation.txt
Novosad, J.
27/5/2012
Keywords keywords.txt
Novosad, J.
27/5/2012
Full text of thesis thesis.pdf
Novosad, J.
27/5/2012
Reader's report posudek_novosad2012.pdf
Strejček, J.
19/6/2012
Appendix 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.