Detail publikace

An Integrated Specification and Verification Technique for Highly Concurrent Data Structures

ABDULLA Parosh A., HAZIZA Frédéric, HOLÍK Lukáš, JONSSON Bengt a REZINE Ahmed. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In: 19th International Conference, TACAS 2013. Lecture Notes in Computer Science, roč. 7795. Berlin Heidelberg: Springer Verlag, 2013, s. 324-338. ISBN 978-3-642-36742-7. ISSN 0302-9743.
Název česky
Integrovaná specifikační a verifikační technika pro vysoce paralelní datové struktury
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)
Jonsson Bengt (Uppsala)
Rezine Ahmed, Assoc. Prof. (LIU)
URL
Klíčová slova

souběžnost,specifikace, ověřování, bezzámkové datové struktury, automaty

Abstrakt

Prezentujeme techniku pro specifikaci a verifikaci paralelních programů, se zaměřením na programy, jejichž korektnost závisí na komplikovaných závislostech lokálních stavů jednotlivých procesů, jako jsou bezzámkové implementace front a zásobníků. Technika staví na automatovém přístupu k model-checkingu, kde je specifikace dána formou automatu, který pozoruje běhy programu a přijímá běhy, které nevyhovují specifikaci. Rozšiřujeme tento přístup zapojením nekonečně stavových automatů, a ukazujeme, jak toto použít pro specifikaci front, zásobníků, množin, apod. Metodu jsme implementovali a otestovali na programech, z nichž některé nebylo dříve možno automaticky verifikovat.

Rok
2013
Strany
324-338
Časopis
Lecture Notes in Computer Science, roč. 7795, ISSN 0302-9743
Sborník
19th International Conference, TACAS 2013
Řada
Lecture Notes in Computer Science
Konference
European Joint Conferences on Theory and Practice of Software -- ETAPS'13 (TACAS'13), Řím, IT
ISBN
978-3-642-36742-7
Vydavatel
Springer Verlag
Místo
Berlin Heidelberg, DE
BibTeX 
@INPROCEEDINGS{FITPUB10230,
   author = "A. Parosh Abdulla and Fr\'{e}d\'{e}ric Haziza and Luk\'{a}\v{s} Hol\'{i}k and Bengt Jonsson and Ahmed Rezine",
   title = "An Integrated Specification and Verification Technique for Highly Concurrent Data Structures",
   pages = "324--338",
   booktitle = "19th International Conference, TACAS 2013",
   series = "Lecture Notes in Computer Science",
   journal = "Lecture Notes in Computer Science",
   volume = 7795,
   number = 0000,
   year = 2013,
   location = "Berlin Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-36742-7",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10230"
}
Nahoru