Cプログラムソースのモデル検査を行うツールです。

概要

• MathSAT4を利用しない「通常版」と利用する「MathSAT利用可能版」を提供します。
• このツールの保証・サポートは有りません。

MathSAT4はUniversity of Trentoで公開されているSMTソルバーで，学術環境における研究や評価の目的にのみ使用可能です。また、書面による許諾なしでは、特に商用製品の一部として使用するなど、商用環境で利用することはできません。

ダウンロード

• readme.txt UTF8
• モデル検査器（通常版）tgz 約5.1MB
• モデル検査器（MathSAT利用可能版）tgz 約5.2MB

実際に利用される場合は、tgzファイル内のREADME, INSTALL, COPYRIGHTも参照ください。

ライセンス

• ライセンスはGPLです。詳細はtgzファイルのCOPYRIGHT, READMEを参照ください。
• MathSATのライセンスについては、こちらを参照ください。

謝辞

JST CREST「実用化を目指した組込みシステム用ディペンダブルオペレーティングシステムの開発」(DEOS)プロジェクトのもと、東京大学によって開発されました。