http://db.cs.berkeley.edu/papers/dbtest12-bloom.pdf http://db.cs.berkeley.edu/papers/dbtest12-bloom.pdf has a really nice extension of this idea - since their l

http://db.cs.berkeley.edu/papers/dbtest12-bloom.pdf http://db.cs.berkeley.edu/papers/dbtest12-bloom.pdf has a really nice extension of this idea - since their language is unordered by default and has only a few explicit ordered primitives, they can use an SMT solver to determine which event interleavings cannot possibly affect the result. This lets them generate schedules that more efficiently explore the space of all possible schedules and find bugs faster.