Zaks et al. employ SPIN on C programs [1]}.
They take advantage of the compiled LLVM byte code of
the target application and SPIN, to consider
all interleavings of reads and writes among shared variables.
While multithreaded operations are seen at assembly level, they
are treated as an atomic operation, called a superstep.
Their supersteps are roughly comparable to the transitions
used here. The work also employs DPOR [2]}.
Their experiments with the dining philosophers problem is limited to
5 philosophers, involving 25,021 supersteps.
