« 『Yices』によるSMTソルバ | トップページ | CCCC(C AND C++CODE COUNTER)GUIランチャーの公開 »

2017年1月19日 (木)

作成したYicesのGUIからオプションを変えSMTを行う

『Yices』でSMTを行う際にオプションが幾つかあるが,それを変更してSMTをしました。
 
スクリプトを組むだけでなく,モデルから検証対象内容を変換させてSMTにかけることもできますので,次回実施する予定です。

Yices2


Yicesl


|

« 『Yices』によるSMTソルバ | トップページ | CCCC(C AND C++CODE COUNTER)GUIランチャーの公開 »

「パソコン・インターネット」カテゴリの記事