This paper nicely brings together ideas from property-based testing (in the style of QuickCheck) with other important ideas from verification, and uses it to build really cool automation. I think it's a great example of how testing and verification can each enrich the other. Plus it's a cool application of Ltac2.
Please note that this is due the morning before class, so that we can discuss it in person. And please install the artifact before Thursday's class.