All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

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