Detail publikace

An Integrated Specification and Verification Technique for Highly Concurrent Data Structures

HOLÍK, L.; ABDULLA, P.; HAZIZA, F.; JONSSON, B.; REZINE, A. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. 19th International Conference, TACAS 2013. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Berlin Heidelberg: Springer Verlag, 2013. p. 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
anglicky
Autoři
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Abdulla Parosh
Haziza Frédéric
Jonsson Bengt
Rezine Ahmed, Assoc. Prof.
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, č. 0000, ISSN 0302-9743
Sborník
19th International Conference, TACAS 2013
Řada
Lecture Notes in Computer Science
ISBN
978-3-642-36742-7
Vydavatel
Springer Verlag
Místo
Berlin Heidelberg
BibTeX 
@inproceedings{BUT103444,
  author="Lukáš {Holík} and Parosh {Abdulla} and Frédéric {Haziza} and Bengt {Jonsson} and Ahmed {Rezine}",
  title="An Integrated Specification and Verification Technique for Highly Concurrent Data Structures",
  booktitle="19th International Conference, TACAS 2013",
  year="2013",
  series="Lecture Notes in Computer Science",
  journal="Lecture Notes in Computer Science",
  volume="7795",
  number="0000",
  pages="324--338",
  publisher="Springer Verlag",
  address="Berlin Heidelberg",
  isbn="978-3-642-36742-7",
  issn="0302-9743",
  url="http://link.springer.com/chapter/10.1007%2F978-3-642-36742-7_23"
}
Nahoru