<?xml version="1.0" encoding="UTF-8"?>
<rdf:RDF xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
         xmlns:dc="http://purl.org/dc/terms/"
         xmlns:foaf="http://xmlns.com/foaf/0.1/"
         xmlns:bibo="http://purl.org/ontology/bibo/"
         xmlns:fabio="http://purl.org/spar/fabio/"
         xmlns:owl="http://www.w3.org/2002/07/owl#"
         xmlns:event="http://purl.org/NET/c4dm/event.owl#"
         xmlns:ore="http://www.openarchives.org/ore/terms/">

    <rdf:Description rdf:about="https://research-explorer.ista.ac.at/record/10190">
        <ore:isDescribedBy rdf:resource="https://research-explorer.ista.ac.at/record/10190"/>
        <dc:title>Value-centric dynamic partial order reduction</dc:title>
        <bibo:authorList rdf:parseType="Collection">
            <foaf:Person>
                <foaf:name></foaf:name>
                <foaf:surname></foaf:surname>
                <foaf:givenname></foaf:givenname>
            </foaf:Person>
            <foaf:Person>
                <foaf:name></foaf:name>
                <foaf:surname></foaf:surname>
                <foaf:givenname></foaf:givenname>
            </foaf:Person>
            <foaf:Person>
                <foaf:name></foaf:name>
                <foaf:surname></foaf:surname>
                <foaf:givenname></foaf:givenname>
            </foaf:Person>
        </bibo:authorList>
        <bibo:abstract>The verification of concurrent programs remains an open challenge, as thread interaction has to be accounted for, which leads to state-space explosion. Stateless model checking battles this problem by exploring traces rather than states of the program. As there are exponentially many traces, dynamic partial-order reduction (DPOR) techniques are used to partition the trace space into equivalence classes, and explore a few representatives from each class. The standard equivalence that underlies most DPOR techniques is the happens-before equivalence, however recent works have spawned a vivid interest towards coarser equivalences. The efficiency of such approaches is a product of two parameters: (i) the size of the partitioning induced by the equivalence, and (ii) the time spent by the exploration algorithm in each class of the partitioning. In this work, we present a new equivalence, called value-happens-before and show that it has two appealing features. First, value-happens-before is always at least as coarse as the happens-before equivalence, and can be even exponentially coarser. Second, the value-happens-before partitioning is efficiently explorable when the number of threads is bounded. We present an algorithm called value-centric DPOR (VCDPOR), which explores the underlying partitioning using polynomial time per class. Finally, we perform an experimental evaluation of VCDPOR on various benchmarks, and compare it against other state-of-the-art approaches. Our results show that value-happens-before typically induces a significant reduction in the size of the underlying partitioning, which leads to a considerable reduction in the running time for exploring the whole partitioning.</bibo:abstract>
        <bibo:volume>3</bibo:volume>
        <dc:publisher>ACM</dc:publisher>
        <dc:format>application/pdf</dc:format>
        <ore:aggregates rdf:resource="https://research-explorer.ista.ac.at/download/10190/10278/2019_ACM_Chatterjee.pdf"/>
        <bibo:doi rdf:resource="10.1145/3360550" />
        <ore:similarTo rdf:resource="info:doi/10.1145/3360550"/>
    </rdf:Description>
</rdf:RDF>
