Approximating Happens-Before Order: Interplay between Static Analysis and State Space Traversal

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F14%3A10279702" target="_blank" >RIV/00216208:11320/14:10279702 - isvavai.cz</a>

Výsledek na webu

<a href="http://doi.acm.org/10.1145/2632362.2632365" target="_blank" >http://doi.acm.org/10.1145/2632362.2632365</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/2632362.2632365" target="_blank" >10.1145/2632362.2632365</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Approximating Happens-Before Order: Interplay between Static Analysis and State Space Traversal

Popis výsledku v původním jazyce

Techniques and tools for verification of multi-threaded programs must cope with the huge number of possible thread interleavings. Tools based on systematic exploration of a program state space employ partial order reduction to avoid redundant thread interleavings. The key idea is to make non-deterministic thread scheduling choices only at statements that read or modify the global state shared by multiple threads. We focus on the approach to partial order reduction used in tools such as Java Pathfinder (JPF), which construct the program state space on-the-fly, and therefore can use only information available in the current program state and execution history to identify statements that may be globally-relevant. In our previous work, we developed a fieldaccess analysis that provides information about fields that may be accessed during program execution, and used it in JPF for more precise identification of globally-relevant statements. We build upon that and propose a may-happen-before

Název v anglickém jazyce

Approximating Happens-Before Order: Interplay between Static Analysis and State Space Traversal

Popis výsledku anglicky

Techniques and tools for verification of multi-threaded programs must cope with the huge number of possible thread interleavings. Tools based on systematic exploration of a program state space employ partial order reduction to avoid redundant thread interleavings. The key idea is to make non-deterministic thread scheduling choices only at statements that read or modify the global state shared by multiple threads. We focus on the approach to partial order reduction used in tools such as Java Pathfinder (JPF), which construct the program state space on-the-fly, and therefore can use only information available in the current program state and execution history to identify statements that may be globally-relevant. In our previous work, we developed a fieldaccess analysis that provides information about fields that may be accessed during program execution, and used it in JPF for more precise identification of globally-relevant statements. We build upon that and propose a may-happen-before

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2014

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 statě ve sborníku

21st International Symposium on Model Checking of Software (SPIN 2014)

ISBN

978-1-4503-2452-6

ISSN

—

e-ISSN

—

Počet stran výsledku

10

Strana od-do

1-10

Název nakladatele

ACM

Místo vydání

USA

Místo konání akce

USA

Datum konání akce

21. 7. 2014

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—