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: https://drops.dagstuhl.de/opus/volltexte/2015/5605/
Abdulla, Parosh A. ; Haziza, Fréderic ; Holík, Lukáš
View Abstraction – A Tutorial (Invited Paper)
| pdf-format: |
|
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 | |
| Seminar: | 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) | |
| Issue date: | 2015 | |
| Date of publication: | 03.12.2015 |
