問題タブ [key-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.
verification - Key検証ツールはどこで光りますか?
KeYの強みを示すコード例は何ですか?
詳細
非常に多くの Formal Method ツールが利用できる中で、KeY が競合他社よりも優れている点はどこでしょうか? いくつかの読みやすいコード例は、比較と理解に非常に役立ちます。
アップデート
KeY の Web サイトを検索すると、本からコード例が見つかりました。適切なコード例がどこかにありますか?
さらに、KeY さんが Java 8 の mergeCollapse in TimSort で見つけたバグに関する論文を見つけました。KeY の強みを示す TimSort の最小限のコードは何ですか? ただし、モデル チェックでバグを検出できないと思われる理由がわかりません。64 要素のビット配列は大きすぎて処理できません。他の演繹的検証ツールでもバグを見つけることができますか?
適切なコード例を使用した確立された検証コンペティションはありますか?
z3 - Z3 ソルバーを KeY 2.8.0 に接続中にエラーが発生しました。コマンドラインで
私は KeY を初めて使用し、検証手順を開始できるようにすべてをセットアップしようとしています。そのためには、SMT Solver: Z3 を有効にする必要があります。Z3 ファイルをダウンロードしましたが、コマンド ラインで Z3 設定のディレクトリ パスを入力すると、KeY で "null" というエラーが表示されます (スクリーンショットを参照)。Z3.exe ファイルのさまざまな場所を試しましたが、同じエラーが発生します。ファイルに移動してディレクトリパスを取得しました->右クリック->オプションキー（macbook）を押します->パスをコピーします。
私が間違っていることを知っている人はいますか？
前もって感謝します！
エラーのスクリーンショット (プライバシー保護のため名前は削除されています)
