--- res: bibo_abstract: - 'Stateless model checking (SMC) is one of the standard approaches to the verification of concurrent programs. As scheduling non-determinism creates exponentially large spaces of thread interleavings, SMC attempts to partition this space into equivalence classes and explore only a few representatives from each class. The efficiency of this approach depends on two factors: (a) the coarseness of the partitioning, and (b) the time to generate representatives in each class. For this reason, the search for coarse partitionings that are efficiently explorable is an active research challenge. In this work we present RVF-SMC , a new SMC algorithm that uses a novel reads-value-from (RVF) partitioning. Intuitively, two interleavings are deemed equivalent if they agree on the value obtained in each read event, and read events induce consistent causal orderings between them. The RVF partitioning is provably coarser than recent approaches based on Mazurkiewicz and “reads-from” partitionings. Our experimental evaluation reveals that RVF is quite often a very effective equivalence, as the underlying partitioning is exponentially coarser than other approaches. Moreover, RVF-SMC generates representatives very efficiently, as the reduction in the partitioning is often met with significant speed-ups in the model checking task.@eng' bibo_authorlist: - foaf_Person: foaf_givenName: Pratyush foaf_name: Agarwal, Pratyush foaf_surname: Agarwal - foaf_Person: foaf_givenName: Krishnendu foaf_name: Chatterjee, Krishnendu foaf_surname: Chatterjee foaf_workInfoHomepage: http://www.librecat.org/personId=2E5DCA20-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0002-4561-241X - foaf_Person: foaf_givenName: Shreya foaf_name: Pathak, Shreya foaf_surname: Pathak - foaf_Person: foaf_givenName: Andreas foaf_name: Pavlogiannis, Andreas foaf_surname: Pavlogiannis foaf_workInfoHomepage: http://www.librecat.org/personId=49704004-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0002-8943-0722 - foaf_Person: foaf_givenName: Viktor foaf_name: Toman, Viktor foaf_surname: Toman foaf_workInfoHomepage: http://www.librecat.org/personId=3AF3DA7C-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0001-9036-063X bibo_doi: 10.1007/978-3-030-81685-8_16 bibo_volume: '12759 ' dct_date: 2021^xs_gYear dct_identifier: - UT:000698732400016 dct_isPartOf: - http://id.crossref.org/issn/0302-9743 - http://id.crossref.org/issn/1611-3349 - http://id.crossref.org/issn/978-3-030-81684-1 dct_language: eng dct_publisher: Springer Nature@ dct_title: Stateless model checking under a reads-value-from equivalence@ ...