@inproceedings{ShilovYi00elsewhere,
  author = "Nikolay Shilov and Kwangkeun Yi",
  title = "Puzzles for Learning Model Checking, Model Checking for Programming Puzzles, Puzzles for Testing Model Checkers",
  booktitle = "Formal Methods *ELSEWHERE* , a Satellite Workshop of FORTE-PSTV-2000",
  pages = "18-37",
  address = "Pisa, Italy",
  year = "2000",
  note = "Final version in v. 43 of {\it Electronic Notes in Theoretical Computer Science} \cite{ShilovYi01elsewhere}"
}