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或瑞典研究委员会的观点。