Detail publikace

Block Me If You Can! Context-Sensitive Parameterized Verification

ABDULLA, P.; HAZIZA, F.; HOLÍK, L. Block Me If You Can! Context-Sensitive Parameterized Verification. In 21st International Static Analysis Symposium. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2014. p. 1-17. ISBN: 978-3-319-10935-0. ISSN: 0302-9743.
Název česky
Zablokuj mě jestli můžeš! Prametrická verifikace citlivá na kontext
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Abdulla Parosh
Haziza Frédéric
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
URL
Klíčová slova

parameterized systems verification paralelism concurrency abstraction well-quasi ordering

Abstrakt

Článek představuje metodu pro automatickou verifikaci systémů s parametrickým počtem komunikujících procesů, jako jsou protokoly pro vzájemné vyloučení. Za tímto účelem jsme navrhli efektivní a přesnou abstrakci.  Metoda je obecnější než metody specializující se na dobře quasi-uspořádané systémy. Experimentálně jsme ověřili její efektivitu. Byli jsme schopni zverifikovat některé systémy, které dříve nebyly automaticky verifikovány, jako například plná verze Szymanského algoritmu pro vzájemné vyloučení.

Anotace

Článek představuje metodu pro automatickou verifikaci systémů s parametrickým počtem komunikujících procesů, jako jsou protokoly pro vzájemné vyloučení.  Za tímto účelem jsme navrhli efektivní a přesnou abstrakci.  Metoda je obecnější než metody specializující se na dobře quasi-uspořádané systémy. Experimentálně jsme ověřili její efektivitu. Byli jsme schopni zverifikovat některé systémy, které dříve nebyly automaticky verifikovány, jako například plná verze Szymanského algoritmu pro vzájemné vyloučení.

Rok
2014
Strany
1–17
Časopis
Lecture Notes in Computer Science, roč. 2014, č. 8723, ISSN 0302-9743
Sborník
21st International Static Analysis Symposium
Řada
Lecture Notes in Computer Science
ISBN
978-3-319-10935-0
Vydavatel
Springer Verlag
Místo
Berlin
DOI
UT WoS
000360204700001
EID Scopus
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"
}
Nahoru