Publication detail

Block Me If You Can! Context-Sensitive Parameterized Verification

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

Original Title

Block Me If You Can! Context-Sensitive Parameterized Verification

Type

conference paper

Language

English

Original Abstract

We present a method for automatic verification of systems with a parameterized number of communicating processes, such as mutual exclusion protocols or agreement protocols. To that end, we present a powerful abstraction framework that uses an efficient and precise symbolic encoding of (infinite) sets of configurations. In particular, it generalizes downward-closed sets that have successfully been used in earlier approaches to parameterized verification. We show experimentally the efficiency of the method, on various examples, including a fine-grained model of Szymanski's mutual exclusion protocol, whose correctness, to the best of our knowledge, has not been proven automatically by any other existing methods.

Keywords

parameterized systems verification paralelism concurrency abstraction well-quasi ordering

Authors

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

RIV year

2014

Released

11. 11. 2014

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-319-10935-0

Book

21st International Static Analysis Symposium

Edition

Lecture Notes in Computer Science

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Year of study

2014

Number

8723

State

Federal Republic of Germany

Pages from

1

Pages to

17

Pages count

17

URL

http://link.springer.com/chapter/10.1007%2F978-3-319-10936-7_1

BibTex

@inproceedings{BUT111638,
  author="Parosh {Abdulla} and Frédéric {Haziza} and Lukáš {Holík}",
  title="Block Me If You Can! Context-Sensitive Parameterized Verification",
  booktitle="21st International Static Analysis Symposium",
  year="2014",
  series="Lecture Notes in Computer Science",
  journal="Lecture Notes in Computer Science",
  volume="2014",
  number="8723",
  pages="1--17",
  publisher="Springer Verlag",
  address="Berlin",
  doi="10.1007/978-3-319-10936-7\{_}1",
  isbn="978-3-319-10935-0",
  issn="0302-9743",
  url="http://link.springer.com/chapter/10.1007%2F978-3-319-10936-7_1"
}