問題タブ [formal-verification]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
z3 - Z3 でメモリ バッファを表現する最も効率的な方法
Z3 で固定サイズのメモリ バッファとそのアクセス操作をモデル化したいと考えています。バッファーのサイズは、数バイトから数百バイトの範囲です。いくつかの既存のツール (KLEE など) で採用されている標準的な方法は、ビットベクトルのドメインと範囲にわたって配列変数を作成することです。各メモリ バッファはそのような配列を取得し、メモリの読み取り/書き込みはselect
/store
操作を使用してエンコードされます。
残念ながら、私のベンチマークでは、このアプローチを使用すると、Z3(*) は一貫して STP よりも遅いように見えます。何が起こっているのかを理解するためにクエリをより詳細に分析する前に、Z3 でメモリ操作をエンコードするための「正しい」アプローチを使用していることを確認したかった (確かに、STP は配列とビットベクトルで使用するように特別に設計されているため) )。
では、Z3 でメモリ バッファを表現する最も効率的な方法は何でしょうか? これまでのところ、いくつかの代替案を検討しています。
store
ネストされた-sを使用する代わりに、アサーションを使用してメモリ バッファーの初期値を指定します。ただし、私の予備テストでは、これにより Z3 がさらに遅くなるようです。- ビットベクトルを使用してバッファをエンコードします。ただし、結果として得られるビットベクトルは非常に大きくなる可能性があり (約 1000 ビット)、Z3 や他のソルバーがそれを効率的に処理できるかどうかはわかりません。
- メモリ バイトごとに個別のビットベクトル変数を作成し、ネストされた
ite
式を使用してメモリ アクセスを対応する変数にルーティングします。ただし、これによりモデルが非常に複雑になり、量指定子が必要になるのではないかと心配しています。 - 配列の代わりに解釈されない関数を使用しますが、これには、Z3 独自の組み込み配列理論よりも効率が悪い方法で配列公理を再定義する必要があります。
私が見逃しているより良いアプローチはありますか?
(*) デフォルトの非インクリメンタル ソルバー、Z3 ブランチunstable@aba79802cfb5
theorem-proving - Owicki-Gries メソッドの理解に助けが必要
私は (誤って) 並行プログラムの検証に関するコースを受講しており、これまで「Owicki-Gries 法」と呼ばれるこの方法について説明してきました。どうやら、アサーションを各ステートメントに関連付けることで、プログラムに関するさまざまな結果を証明し、これらのアサーションが帰納的であり、互いに干渉しないことを示すことができます。私たちの課題の 1 つは、Lamports の Fast Mutual Exclusion アルゴリズムに関するもので、この論文で詳しく説明しています。
この論文では、相互排除のための Owicki-Gries スタイルの証明が与えられています。それは完全に直感に反するように見えます。私が理解するのに苦労しているのは、そもそもこれらの主張をどのように考え出すかということですか? これらの主張が強すぎず (干渉の自由を壊すほど強い) も弱すぎもしない (たとえば、各ステートメントのトートロジーのような些細なこと) はいつわかりますか?
乾杯
tdd - テスト駆動開発を検証できますか?
テスト駆動開発は正式に検証できますか? プログラムが正しく、適切に動作するという保証はありますか? テストを選択するための正式な根拠はありますか? それに従うアルゴリズムはありますか?
formal-methods - ループ不変条件と最弱前提条件の関係は何ですか
ウィキペディアがリストするループ不変条件を考えると、ループの最も弱い前提条件を生成する良い方法 ( http://en.wikipedia.org/wiki/Predicate_transformer_semanticsから):
M[x <- N] は、M 内のすべての x を N に置き換えます。
さて、私の問題は変数 y です。\forall y, は式で y をバインドするため、「y は新しい変数のタプルです」は解析されません。"[x <- y]" の y と同じように、y は \forall でバインドされていますか? 上記を解析することはできません。
編集:参照要求を避けるために言い換えました。
私の質問は、ループ不変条件と最も弱い前提条件の計算との間の直接的な関係は何かということです。実際に行われている多くのことは、ループの最も弱い前提条件を検証に適した前提条件に緩和しているようです。ウィキペディアの上記は、ループ不変条件が与えられた場合、鼻の最も弱い前提条件を実際に計算できることを示唆していますが、この条件を理解するのに苦労しています。
haskell - このGHCコアの「証明」をどう読むか?
この小さな Haskell を書いて、GHC が自然数の場合、偶数は半分しかできないことをどのように証明するかを理解しました。
コアの関連部分は次のようになります。
Flip 型ファミリのインスタンスを介して型をキャストする一般的な流れは知っていますが、完全には理解できないことがいくつかあります。
- とはどういう意味
@~ <Nat.Flip x_apH>_N
ですか? x の Flip インスタンスですか? それは とどう違うの@ (Nat.Flip x_apH)
ですか? 私は両方に興味が< >
あります_N
の最初のキャストについてhalve
:
- とは何
dt_dK6
の略ですか? ある種の等価証明であることは理解していますが、どれがどれでしょうか?dt1_dK7
dt2_dK8
Sym
等価性を逆方向に実行することを理解しています- は何をし
;
ますか?等価証明は順番に適用されていますか? - これら
_N
と_R
接尾辞は何ですか? - Flip のインスタンスと
TFCo:R:Flip[0]
は?TFCo:R:Flip[1]
testing - concolic テストでは、「具体的な実行」とはどういう意味ですか?
concolic testingの概念を調べていたときに、「concrete & symbolic execution」という用語に出くわしました。(そこで言及されている記事、「CUTE: A concolic unit testing engine for C」では、抽象セクションでその用語が使用されています。)
「使用されたアプローチは、シンボリック実行と具象実行を組み合わせた以前の研究に基づいており、より具体的には、そのような組み合わせを使用してテスト入力を生成し、実行可能なすべての実行パスを探索します。」
「具体的な実行」が何を意味するのか、誰でも確認できますか?私の検索にもかかわらず、直接の引用/明示的なステートメントを見つけることができませんでした.
私が理解していることから、「具体的な実行」とは、「変数や入力などに記号値を想定する記号実行とは異なり、実際の入力値を使用してプログラムを実行すること」を意味します。私が間違っている場合は、修正してください(可能であれば小さな例で)。