問題タブ [formal-verification]

多くの論文を読んだ後、CCuredソース (またはバイナリ) を見つけて、C ソース コードで使用しようとしています。

ただし、すべてのリンクが無効になっているようです。いくつかのグーグルの後、私はここで尋ねています。万が一あなたのハード ドライブに tarball があった場合、誰かがそれら (ソース、ドキュメントなど) をアップロードしてくれませんか?

編集: 著者の 1 人にもメールを送信しましたが、まだ応答がありません。しばらくして他の人にメールを送信してみます。

（紙面引用）

既存の C プログラムに型の安全性を保証するプログラム変換システムを CCured しました。CCured は、メモリ エラーが発生しないことを静的に検証しようとし、静的検証が不十分な場合にランタイム チェックを挿入します。既存の C プログラムに適切なポインターの種類を推測します。CCured は、物理サブタイピングを使用して、コンパイル時に多数の型キャストを認識および検証します。追加の型キャストは、実行時の型情報を使用して検証されます。

FFS のソフトウェア実装を検証しようとしています。FFS の機能は、数値の最下位ビットのインデックス位置 (1 から始まる) を返すことです。ゴースト変数を使用するなど、さまざまな方法で試しました。ジェシーはそれを確認できず、理由がわかりませんか? いくつかの指針は本当に役に立ちます。これがコードのサンプルです。8ビットの数値を想定しています。

プログラムにバグがあることを証明できるという事実について考えていました。テストして、多かれ少なかれバグ耐性があるかどうかを評価できます。

しかし、プログラムにバグがないことを (理論的にも) 証明する方法はありますか?

「Hello World」などの単純なプログラムの場合は、できるはずです。しかし、より大きなプログラムはどうでしょうか?

次のLTLプロパティの単純なPromelaモデルをモデルチェックしようとしています:

そして、エラーが発生しました。エラートレイルのガイド付きシミュレーションでは、次の出力が得られます。

ここで、「M[0] until M[1]」がどこで違反されているのかわかりません。M[0] は init プロセスで 1 に設定され、M[1] が 1 になるまでそのままです。トレースが非常に早く終了するか、「stronguntil」のセマンティクスを完全に誤解している可能性があります。私はこれが事実であると確信しています...しかし、私は何が間違っていますか? Promela ファイル内の LTL の指定は大丈夫ですか?

問題のモデルは次のとおりです (単純なペトリネット)。

このシナリオを単純化します (これは Perfect Developer にあり、すぐに複雑になります)。クラスに という単純なスキーマがあるとします。これは、(以前に定義されたクラス) をパラメーターとしてSucceed受け取ります。Course

基本的に、コースが前提条件として自分のコースにあることを確認してから、事後条件のセットにset追加します。coursesCompletedこの単純なスキーマはうまく機能し、次のようになります。

ただし、非常に単純なif条件を追加したいと思います。自分の courseCompleted カーディナリティが 30 以上の場合、Diplomation列挙型を " Ok" に設定します。カーディナリティが 30 未満の場合は、" NotOk"に設定します

Perfect Developer のドキュメント、および私が見たすべてのまれな例によると、if構文は次のようになります。

ただし、スキーマに直接プラグインすると、次のようになります。

それは機能しません、私はいつも「非常に説明的」になります

エラー！キーワード 'if' に構文エラーがあります。次のいずれかが必要です: '!' '(''?''c_address_of'

;どこにでも追加したり、 の後viaにキーワードを追加したり、post位置を変更したり、 と を交換したり;、,その他多くの試行錯誤を試みました。

私の質問は次のとおりです: ifPerfect Developer で、スキーマの事後条件に条件を追加するにはどうすればよいですか?

Perfect Developerでお答えください。私は（悲しいことに）自分の正式な方法を知っています。必要なのifは、世界で最悪のツールでコンパイルすることだけです。

たとえば、ビットベクトルの 3 番目のビットが 0 であるかどうかをテストするブール変数が必要です。ビットベクトルの理論では、1 ビットをビットベクトルとして抽出できますが、ブール型では抽出できません。このキャストができるかな。ありがとうございました。

===更新===

私の質問が明確でない場合は申し訳ありません。しかし、Nikolaj Bjorner の答えは、ビット ベクトルの特定のビットをテストする方法です。ビットベクトルの最初のビットの値を変数に代入したいのですが。この例を次のように変更してみます。

そしてz3は不平を言います：

後で使用するために、その変数 bit0 が必要です。ヒントを教えてください。ありがとう。