License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.SynCoP.2015.1
URN: urn:nbn:de:0030-drops-56057
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5605/
Abdulla, Parosh A. ;
Haziza, Fréderic ;
Holík, Lukáš
View Abstraction – A Tutorial (Invited Paper)
Abstract
We consider parameterized verification, i.e., proving correctness of a system with an unbounded number of processes. We describe the method of view abstraction whose aim is to provide a small model
property, i.e., showing correctness by only inspecting instances of the system consisting of a small fixed number of processes. We illustrate the method through an application to the classical
Burns' mutual exclusion protocol.
BibTeX - Entry
@InProceedings{abdulla_et_al:OASIcs:2015:5605,
author = {Parosh A. Abdulla and Fr{\'e}deric Haziza and Luk{\'a}{\v{s}} Hol{\'i}k},
title = {{View Abstraction – A Tutorial (Invited Paper)}},
booktitle = {2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15)},
pages = {1--15},
series = {OpenAccess Series in Informatics (OASIcs)},
ISBN = {978-3-939897-82-8},
ISSN = {2190-6807},
year = {2015},
volume = {44},
editor = {{\'E}tienne Andr{\'e} and Goran Frehse},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5605},
URN = {urn:nbn:de:0030-drops-56057},
doi = {10.4230/OASIcs.SynCoP.2015.1},
annote = {Keywords: program verification, model checking, parameterized systems}
}
Keywords: |
|
program verification, model checking, parameterized systems |
Collection: |
|
2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) |
Issue Date: |
|
2015 |
Date of publication: |
|
03.12.2015 |