Thanks for producing this video, it solidified a lot of unknowns for me about CHESS. There is one thing I'm still curious about, though -- in what contexts can CHESS be run? Based on the video, it sounds as if CHESS can only be used with defined unit tests -- is this correct? I would like to be able to use CHESS on a running program, but I'm guessing this is not possible since it would not allow CHESS to "re-run" the program with different pre-emption scenarios. Is this true?