モデル検査のパズル化: パズルを用いたプログラム検証アルゴリズムの体験

摘要

小学生から大人までが来訪する研究宰公開では，実際に行われいる研究を極力単純化し，専門知識がなくてもわかるように嚙み砕いて説明する必要がある.形式言語理論やそれを利用したプログラム検おの研究を進めている著者の研究室では，2018年に実施された研究室公開において，「無限の可能性を有限で網羅する」というキャッチフレーズのもと，条件を满たす新幹線を完成させるタイリングパズルを作成し，それを利用してプログラム検証アルゴリズムを体験してもらった.今冋，コンピュータ教育をテーマとする夏のプログラミング•シンポジウムにおいて，その研究室公開の内容を模擬授業という形で実践し，解説を行った.本稿ではその実施内容をまとめ，会場での質疑とそれに対する冋答について報告する.