Approximating Happens-Before Order: Interplay between Static Analysis and State Space Traversal
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
Approximating Happens-Before Order: Interplay between Static Analysis and State Space Traversal
Original language description
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
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2014
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
21st International Symposium on Model Checking of Software (SPIN 2014)
ISBN
978-1-4503-2452-6
ISSN
—
e-ISSN
—
Number of pages
10
Pages from-to
1-10
Publisher name
ACM
Place of publication
USA
Event location
USA
Event date
Jul 21, 2014
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—