Nikolay V. Shilov and Kwangkeun Yi
"Training sessions are good opportunities to present students with
challenging programming problems that cannot be solved without theoretical background in spite of simple formulation. The trainers should provide students with background theory as soon as students realize the programming complexity of these problems."
- Kwangkeun Yi's site has a lot of papers on formal methods. Puzzles for Learning Model Checking, Model Checking for Programming Puzzles, Puzzles for Testing Model Checkers seems interesting.