VSTTE Competition - ソフトウェア検証コンテストにチームTebasakiという名前で参加した。
VSTTE (Verified Software: Theories, Tools and Experiments) 2012 という学会の併設イベントでソフトウェア検証コンテストというものが開催されることを前日に id:keigoi さんに教えてもらって参加してみた。日時は日本時間で11月9日の0時から48時間。初めて競技プログラミング(プルービング?)に参加したがよい経験になったと思う。
メンバーは id:mzpさん、@pirapiraさん、@hirose_golfさんの4名。チーム名は@pirapiraさんの提案で名古屋っぽいものがよいということでいろいろ候補を挙げて結局Tebasaki (手羽先) に決定。使う検証器や実装言語は何でも良い！ということだったので我々はCoqを使った。コンペ中はプライベートにしておいて後で公開するというためにソースコード管理はbitbucket.org上にリポジトリを置き、gitを使った。しかし、@pirapiraさんはオランダに引っ越したばかりでネットワーク回線がiPhoneしかなく、また、@hirose_golfさんもgitに慣れていないということで、結局私と@mzpだけがコミットした。
以下は感想:
- 0時に開催ということで直前の22:00くらいは寝て、0時に起きて、その後5:00くらいに寝てということをやったため、生活のリズムが狂ってしまった。
- 合宿みたいにして寝ずにやろうと思ったが、やはり集中力のために睡眠は重要なのでちゃんと家に帰って寝た方がよいと思った。
- 難しかったけれど楽しかった。
最後に、証明器や検証器について興味があるけどなかなか手がでないという方のためにハッカソンします！ ProofのHackathonということでハッシュタグは #proofthon(命名 by mzp)です。
