KeYの強みを示すコード例は何ですか?
詳細
非常に多くの Formal Method ツールが利用できる中で、KeY が競合他社よりも優れている点はどこでしょうか? いくつかの読みやすいコード例は、比較と理解に非常に役立ちます。
アップデート
KeY の Web サイトを検索すると、本からコード例が見つかりました。適切なコード例がどこかにありますか?
さらに、KeY さんが Java 8 の mergeCollapse in TimSort で見つけたバグに関する論文を見つけました。KeY の強みを示す TimSort の最小限のコードは何ですか? ただし、モデル チェックでバグを検出できないと思われる理由がわかりません。64 要素のビット配列は大きすぎて処理できません。他の演繹的検証ツールでもバグを見つけることができますか?
適切なコード例を使用した確立された検証コンペティションはありますか?