jayhorn

マスター
展開

ジャワとホーン条項

Jayhornは、Javaのソフトウェアモデルチェックツールです。 Jayhornは、Javaプログラムの特定の悪い状態が決して到達できないという証拠を見つけようとします。これらの悪い状態は、ランタイムアサーションを追加することで指定されます（たとえば、オブジェクト参照がアクセスする前にnullであってはならないといういくつかのアサーションが生成される場合があります）。

Jayhornは、精度の側面に誤りを犯そうとします。つまり、主張が常に保持されていることを証明できない場合、アサーションが違反される可能性があると主張します（これは健全性と呼ばれます）。 Jayhornは現在、単一のスレッドを使用し、動的なクラスの読み込みがなく、静的イニシャル化剤で複雑な操作を実行しないJavaの健全（Modulo Bugs）です。

Jayhornをダウンロードして実行する方法については、当社のWebサイトをチェックしてください。 Jayhornの実装方法については、Jayhorn Developmentブログをご覧ください。

チャットに参加してください

クイックガイド

./gradlew assemble
java -jar jayhorn/build/libs/jayhorn.jar -help
java -jar jayhorn/build/libs/jayhorn.jar -j example/classes -solution -trace

豊かさの声明

このプロジェクトは、豊かさの精神で行われました。実用的なプログラム分析を構築するときは、多くの場合、角を切る必要があります。部分的にのみサポートしたりサポートしたりしない言語機能についてオープンにするために、この堅実さの声明を添付しています。

私たちの分析には、次の機能の完全な健全な取り扱いはありません。

• JNI、暗黙的な方法の呼び出し（ファイナライザー、クラス初期化剤、スレッド。<init>など）
• 整数オーバーフロー
• それに関連する例外とフロー
• 反射API（例、method.invoke（）、class.newinstance）
• Invokedynamic
• 実行時のコード生成、動的荷重
• さまざまなクラスローダー
• 重要なネイティブメソッド（object.run、object.dopriviledeg）

このステートメントは、Soundiness.orgのSudiness Statement Generatorで作成されました。

ライセンス

Jayhornはオープンソースであり、MITライセンスの下で配布されています。

Jayhornで使用されるライブラリには、特に以下が含まれます。

• SOOT、LGPL 2.1以下の下で分布しています。
• BSDライセンスの下で配布されているEldarica。
• プリンセス。これは、LGPL 2.1以下で分布しています。

謝辞と免責事項

Jayhornは部分的に資金提供されています。

• AFRL契約番号FA8750- 15-C-0010。
• 契約FA8750-15-2-0087に基づくDARPA
• NSF賞No. 1422705
• スウェーデン研究評議会の助成金2014-5484

この資料で表明された意見、調査結果、結論、または推奨事項は、著者の意見が必ずしもAFRL、DARPA、NSF、またはスウェーデンの研究評議会の見解を反映しているわけではありません。