Model Checking of Concurrent Programs with Static Analysis of Field Accesses

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F15%3A10281099" target="_blank" >RIV/00216208:11320/15:10281099 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1016/j.scico.2014.10.008" target="_blank" >http://dx.doi.org/10.1016/j.scico.2014.10.008</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1016/j.scico.2014.10.008" target="_blank" >10.1016/j.scico.2014.10.008</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Model Checking of Concurrent Programs with Static Analysis of Field Accesses

Popis výsledku v původním jazyce

Systematic exploration of all possible thread interleavings is a popular approach to detect errors in multi-threaded programs. A common strategy is to use a partial order reduction technique and perform a non-deterministic thread scheduling choice only when the next instruction to be executed may possibly read or modify the global state. However, some verification frameworks and software model checkers, including Java Pathfinder (JPF), construct the program state space on-the-fly during traversal. The partial order reduction technique built into such a tool can use only the information available in the current state to determine whether the execution of a given instruction is globally-relevant. For example, the reduction technique has to make a threadchoice at every field access on a heap object reachable from multiple threads, even in the case of fields that are really accessed only by a single thread during program execution, because it does not have any information about what may h

Název v anglickém jazyce

Model Checking of Concurrent Programs with Static Analysis of Field Accesses

Popis výsledku anglicky

Systematic exploration of all possible thread interleavings is a popular approach to detect errors in multi-threaded programs. A common strategy is to use a partial order reduction technique and perform a non-deterministic thread scheduling choice only when the next instruction to be executed may possibly read or modify the global state. However, some verification frameworks and software model checkers, including Java Pathfinder (JPF), construct the program state space on-the-fly during traversal. The partial order reduction technique built into such a tool can use only the information available in the current state to determine whether the execution of a given instruction is globally-relevant. For example, the reduction technique has to make a threadchoice at every field access on a heap object reachable from multiple threads, even in the case of fields that are really accessed only by a single thread during program execution, because it does not have any information about what may h

Druh

J_x - Nezařazeno - Článek v odborném periodiku (Jimp, Jsc a Jost)

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GP13-12121P" target="_blank" >GP13-12121P: Praktická verifikace programů s použitím kombinace statické a dynamické analýzy</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2015

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

Science of Computer Programming

ISSN

0167-6423

e-ISSN

—

Svazek periodika

98

Číslo periodika v rámci svazku

4

Stát vydavatele periodika

NL - Nizozemsko

Počet stran výsledku

29

Strana od-do

735-763

Kód UT WoS článku

000347741400012

EID výsledku v databázi Scopus

2-s2.0-84954370475