Pick an example from the Examples menu (or write your own program),
then press Verify — or Run to execute it under all thread
interleavings with the reference interpreter.
Verify a program to see the Boogie it generates.
Press Run to execute the program under all interleavings
(the reference interpreter, Melvin’s differential oracle).