jayhorn

掌握
開發

Java和Horn條款

Jayhorn是Java的軟件模型檢查工具。 Jayhorn試圖找到證據，證明Java計劃中的某些壞狀態永遠無法達到。這些不良狀態是通過添加運行時斷言來指定的（如果可以生成某些斷言，例如，在訪問之前不得無效對象引用）。

Jayhorn試圖在精確的一邊犯錯，當無法證明斷言總是存在時，它將聲稱可能會違反斷言（這稱為聲音）。 Jayhorn目前是使用單個線程，沒有動態類加載且不在靜態初始化器中執行複雜操作的Java的聲音（Modulo Bug）。

有關如何下載和運行Jayhorn的信息，請查看我們的網站。有關如何實施Jayhorn的信息，請查看我們的Jayhorn開發博客。

加入聊天

快速指南

./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）
• Invokedymanic
• 運行時代碼生成，動態加載
• 不同的類加載程序
• 關鍵的本機方法（object.run，object.dopileged）

該聲明是通過soundiness.org的shonsiness語句生成器產生的。

許可證

Jayhorn是開源的，並根據MIT許可進行分發。

Jayhorn中使用的庫包括：

• 煙灰，分佈在LGPL 2.1或更高版本下。
• Eldarica，根據BSD許可分發。
• 公主，分佈在LGPL 2.1或更高版本下。

致謝和免責聲明

Jayhorn部分由以下方式資助：

• AFRL合同編號FA8750-15-C-0010。
• DARPA根據協議FA8750-15-2-0087
• NSF獎1422705
• 瑞典研究委員會贈款2014-5484

在本材料中表達的任何意見，發現和結論或建議都是作者的意見，不一定反映了AFRL，DARPA，NSF或瑞典研究委員會的觀點。