Puzzles for Learning Model Checking, Model Checking for Programming Puzzles, Puzzles for Testing Model Checkers
Nikolay V. Shilov, Kwangkeun Yi · Electronic Notes in Theoretical Computer Science · 2001
Paper discusses some issues related to the utility of finite games for early formal methods teaching and for validation of automatic tools which implement formal methods. In particular, some experience with (1) undergraduate teaching model checking via finite games, (2) solving game-based constraints via model checking, (3) testing model checkers against game test suits is presented. Basic ideas are illustrated by a model checking based solution for a complicated puzzle how to identify a unique false coin among given ones balancing them limited times.