Puzzles for Learning Model Checking, Model Checking for Programming Puzzles, Puzzles for Testing Model Checkers

AbstractPaper 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