  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
\emph{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.
