日々の流転

λ. VSTTE 2012 Software Verification Competition

VSTTE 2012 Software Verification Competition というソフトウェア検証のコンテストが開催されている。 都合が合わずに参加できなかったけど、問題文 を見るとそう複雑でもないし、時間のあるときにでもボチボチやってみようと思う。

• <URL:https://github.com/msakai/vstte2012vc>

λ. TPP2011のTPPmarkをZ3で解いてみた

昨日・今日で定理証明のイベント 7th TPP (2011) が開催されている。 私は残念ながら参加できないのだけど、お題(TPPmark)「Uniform Candy Distribution」 をSMTソルバZ3で解いてみた。

• 投稿版
• 最新版レポジトリ＠github

Z3等のSMTソルバは、通常の自動定理証明器や対話的定理証明と比べ、全称量化子や帰納法の取り扱いに制限があるため、その辺りでは苦労したものの、この程度の補助でこれだけ証明できるなら結構使えると感じた。

問題ページで、集まった解答が公開されているが、それを見ると私以外はIsabelle/HOLとCoq(+SSReflect)しか使ってなくて、他のツールの使い手は不甲斐ないなぁと思った。 ACL, PVS, Mizer あたりがいないのは参加者層が偏ってそうだ。 あと、汎用の定理証明ツールではないけど、MaudeやCafeOBJとかでどう扱われるのかとかも見てみたかったかも。