About: LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

AttributesValues
rdf:type
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.
  • 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. (en)
Title
  • LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model
  • LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model (en)
skos:prefLabel
  • LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model
  • LTL Model Checking of Parallel Programs with Under-Approximated TSO Memory Model (en)
skos:notation
  • RIV/00216224:14330/13:00070191!RIV14-MSM-14330___
http://linked.open...avai/riv/aktivita
http://linked.open...avai/riv/aktivity
  • I, P(LG13010)
http://linked.open...vai/riv/dodaniDat
http://linked.open...aciTvurceVysledku
http://linked.open.../riv/druhVysledku
http://linked.open...iv/duvernostUdaju
http://linked.open...titaPredkladatele
http://linked.open...dnocenehoVysledku
  • 85540
http://linked.open...ai/riv/idVysledku
  • RIV/00216224:14330/13:00070191
http://linked.open...riv/jazykVysledku
http://linked.open.../riv/klicovaSlova
  • LTL model checking; divine model checker; relaxed memory model (en)
http://linked.open.../riv/klicoveSlovo
http://linked.open...ontrolniKodProRIV
  • [3001B20CB6B5]
http://linked.open...v/mistoKonaniAkce
  • Barcelona
http://linked.open...i/riv/mistoVydani
  • Barcelona
http://linked.open...i/riv/nazevZdroje
  • Proceedings of Application of Concurrency to System Design, 2013
http://linked.open...in/vavai/riv/obor
http://linked.open...ichTvurcuVysledku
http://linked.open...cetTvurcuVysledku
http://linked.open...vavai/riv/projekt
http://linked.open...UplatneniVysledku
http://linked.open...iv/tvurceVysledku
  • Barnat, Jiří
  • Brim, Luboš
  • Havel, Vojtěch
http://linked.open...vavai/riv/typAkce
http://linked.open.../riv/zahajeniAkce
issn
  • 1550-4808
number of pages
http://bibframe.org/vocab/doi
  • 10.1109/ACSD.2013.8
http://purl.org/ne...btex#hasPublisher
  • IEEE Computer Society
https://schema.org/isbn
  • 9780769550350
http://localhost/t...ganizacniJednotka
  • 14330
Faceted Search & Find service v1.16.118 as of Jun 21 2024


Alternative Linked Data Documents: ODE     Content Formats:   [cxml] [csv]     RDF   [text] [turtle] [ld+json] [rdf+json] [rdf+xml]     ODATA   [atom+xml] [odata+json]     Microdata   [microdata+json] [html]    About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 112 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software