The two papers assigned for today describe a number of techniques for dealing with the challenges of model checking:
For OP2, choose the one technique you found most interesting, describe it briefly, explain what you like about it, and identify one or two limitations. Given the little space afforded by an OP, you might consider devoting one paragraph to the overview of the technique, one paragraph to explaining what got you excited about it, and the remainder of the OP to the description of the limitations. Make sure your argument for the limitations is crisp and persuasive.
Favorite OP2: Cristian's OP