Detail publikace

Block Me If You Can! Context-Sensitive Parameterized Verification

ABDULLA Parosh A., HAZIZA Frédéric a HOLÍK Lukáš. Block Me If You Can! Context-Sensitive Parameterized Verification. In: 21st International Static Analysis Symposium. Lecture Notes in Computer Science, roč. 2014. Berlin: Springer Verlag, 2014, s. 1-17. ISBN 978-3-319-10935-0. ISSN 0302-9743. Dostupné z: http://link.springer.com/chapter/10.1007%2F978-3-319-10936-7_1
Název česky
Zablokuj mě jestli můžeš! Prametrická verifikace citlivá na kontext
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Abdulla Parosh A. (Uppsala)
Haziza Frédéric (Uppsala)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
URL
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
Konference
21st International Static Analysis Symposium -- SAS 2014, Mnichov, DE
ISBN
978-3-319-10935-0
Vydavatel
Springer Verlag
Místo
Berlin, DE
DOI
10.1007/978-3-319-10936-7_1
UT WoS
000360204700001
EID Scopus
2-s2.0-84921744929
BibTeX 
@INPROCEEDINGS{FITPUB10698,
   author = "A. Parosh Abdulla and Fr\'{e}d\'{e}ric Haziza and Luk\'{a}\v{s} Hol\'{i}k",
   title = "Block Me If You Can! Context-Sensitive Parameterized Verification",
   pages = "1--17",
   booktitle = "21st International Static Analysis Symposium",
   series = "Lecture Notes in Computer Science",
   journal = "Lecture Notes in Computer Science",
   volume = 2014,
   number = 8723,
   year = 2014,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-319-10935-0",
   ISSN = "0302-9743",
   doi = "10.1007/978-3-319-10936-7\_1",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10698"
}
Nahoru