Publication result detail

View Abstraction - A Tutorial

HOLÍK, L.; HAZIZA, F.; ABDULLA, P.

Original Title

View Abstraction - A Tutorial

English Title

View Abstraction - A Tutorial

Type

Paper in proceedings (conference paper)

Original Abstract

We consider parameterized verification, i.e., proving correctness of a system with an unboundednumber of processes. We describe the method of view abstraction whose aim is to provide a smallmodel property, i.e., showing correctness by only inspecting instances of the system consistingof a small fixed number of processes. We illustrate the method through an application to theclassical Burns mutual exclusion protocol. 

English abstract

We consider parameterized verification, i.e., proving correctness of a system with an unboundednumber of processes. We describe the method of view abstraction whose aim is to provide a smallmodel property, i.e., showing correctness by only inspecting instances of the system consistingof a small fixed number of processes. We illustrate the method through an application to theclassical Burns mutual exclusion protocol. 

Keywords

parallelism
parameterised systems
view abstraction
verification
well structured transition systems

Key words in English

parallelism
parameterised systems
view abstraction
verification
well structured transition systems

Authors

HOLÍK, L.; HAZIZA, F.; ABDULLA, P.

RIV year

2016

Released

01.11.2015

Publisher

Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik

Location

Dagstuhl

ISBN

978-3-939897-82-8

Book

2nd International Workshop on Synthesis of Complex Parameters

Edition

OpenAccess Series in Informatics

ISBN

2190-6807

Periodical

OpenAccess Series in Informatics (OASIcs)

Volume

44

Number

1

State

Federal Republic of Germany

Pages from

1

Pages to

15

Pages count

15

BibTex

@inproceedings{BUT119935,
  author="Lukáš {Holík} and Frédéric {Haziza} and Parosh {Abdulla}",
  title="View Abstraction - A Tutorial",
  booktitle="2nd International Workshop on Synthesis of Complex Parameters",
  year="2015",
  series="OpenAccess Series in Informatics",
  journal="OpenAccess Series in Informatics (OASIcs)",
  volume="44",
  number="1",
  pages="1--15",
  publisher="Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
  address="Dagstuhl",
  doi="10.4230/OASIcs.SynCoP.2015.1",
  isbn="978-3-939897-82-8",
  issn="2190-6807"
}