LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00070191" target="_blank" >RIV/00216224:14330/13:00070191 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1109/ACSD.2013.8" target="_blank" >http://dx.doi.org/10.1109/ACSD.2013.8</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1109/ACSD.2013.8" target="_blank" >10.1109/ACSD.2013.8</a>
Alternative languages
Result language
angličtina
Original language name
LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model
Original language description
Model checking of parallel programs under relaxed memory models has been so far limited to the verification of safety properties. Tools have been developed to automatically synthesise correct placement of synchronisation primitives to reinstate the sequential consistency. However, in practice it is not the sequential consistency that is demanded, but the correctness of the program with respect to its specification. In this paper, we introduce a new explicit-state Linear Temporal Logic model checking procedure that allows for full verification of programs under approximated Total Store Ordering memory model. We also present a workflow of automated procedure to place the synchronisation primitives into the system under inspection to make it satisfy the given specification under the approximated memory model. Our experimental evaluation has been conducted within DiVinE, our parallel and distributed-memory LTL model checker.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/LG13010" target="_blank" >LG13010: Czech Republic representation in the European Research Consortium for Informatics and Mathematics (ERCIM)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2013
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of Application of Concurrency to System Design, 2013
ISBN
9780769550350
ISSN
1550-4808
e-ISSN
—
Number of pages
9
Pages from-to
51-59
Publisher name
IEEE Computer Society
Place of publication
Barcelona
Event location
Barcelona
Event date
Jan 1, 2013
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—