Detail publikačního výsledku

Block Me If You Can! Context-Sensitive Parameterized Verification

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

Originální název

Block Me If You Can! Context-Sensitive Parameterized Verification

Anglický název

Block Me If You Can! Context-Sensitive Parameterized Verification

Druh

Stať ve sborníku v databázi WoS či Scopus

Originální abstrakt

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.

Anglický abstrakt

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.

Klíčová slova

parameterized systems
verification
paralelism
concurrency
abstraction
well-quasi ordering

Klíčová slova v angličtině

parameterized systems
verification
paralelism
concurrency
abstraction
well-quasi ordering

Autoři

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

Rok RIV

2015

Vydáno

11.11.2014

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-319-10935-0

Kniha

21st International Static Analysis Symposium

Edice

Lecture Notes in Computer Science

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Svazek

2014

Číslo

8723

Stát

Spolková republika Německo

Strany od

1

Strany do

17

Strany počet

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"
}