| Identifikační kód | RIV/00216224:14330/13:00070191 |
|---|
| Název v anglickém jazyce | LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model |
|---|
| Druh | D - Článek ve sborníku |
|---|
| Jazyk | eng - angličtina |
|---|
| Obor - skupina | I - Informatika |
|---|
| Obor | IN - Informatika |
|---|
| Rok uplatnění | 2013 |
|---|
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
|---|
| Počet výskytů výsledku | 1 |
|---|
| Počet tvůrců celkem | 3 |
|---|
| Počet domácích tvůrců | 3 |
|---|
| Výčet všech uvedených jednotlivých tvůrců | Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792)
Luboš Brim (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6500773)
Vojtěch Havel (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3095673) |
|---|
| Popis výsledku v anglickém jazyce | 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. |
|---|
| Klíčová slova oddělená středníkem | LTL model checking; divine model checker; relaxed memory model |
|---|
| Stránka www, na které se nachází výsledek | - |
|---|
| DOI výsledku | 10.1109/ACSD.2013.8 |
|---|