jayhorn
version 0.7
| 주인 | ||||
|---|---|---|---|---|
| 개발 |
자바와 경적 조항
Jayhorn은 Java의 소프트웨어 모델 점검 도구입니다. Jayhorn은 Java 프로그램의 특정 나쁜 상태가 결코 도달 할 수 없다는 증거를 찾으려고합니다. 이러한 나쁜 상태는 런타임 어설 션을 추가하여 지정됩니다 (예를 들어, 액세스하기 전에 객체 참조가 무효가되어서는 안된다는 일부 주장이 생성 될 수 있습니다).
Jayhorn은 정밀한 측면에서 오류를 시도합니다. 즉, 주장이 항상 유지된다는 것을 증명할 수 없을 때, 주장이 위반 될 수 있다고 주장합니다 (이것은 소리라고합니다). Jayhorn은 현재 단일 스레드를 사용하고 동적 클래스로드가 없으며 정적 초기화기에서 복잡한 작업을 수행하지 않는 Java의 경우 현재 사운드 (Modulo Bugs)입니다.
Jayhorn을 다운로드하고 실행하는 방법에 대한 자세한 내용은 웹 사이트를 확인하십시오. 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이 프로젝트는 건전한 정신으로 이루어졌습니다. 실용적인 프로그램 분석을 구축 할 때는 종종 모서리를 자르는 것이 필요합니다. 부분적으로 만 지원하거나 지원하지 않는 언어 기능에 대해 공개되기 위해이 음성 진술을 첨부하고 있습니다.
우리의 분석은 다음 기능에 대한 완전히 사운드 처리가 없습니다.
이 진술은 soundiness.org의 soundiness 문 발전기로 제작되었습니다.
Jayhorn은 오픈 소스이며 MIT 라이센스에 따라 배포됩니다.
Jayhorn에 사용되는 라이브러리에는 특히 다음과 같습니다.
Jayhorn은 다음과 같이 부분적으로 자금을 지원합니다.
이 자료에 표현 된 모든 의견, 결과 및 결론 또는 권장 사항은 저자의 의견이 AFRL, DARPA, NSF 또는 스웨덴 연구위원회의 견해를 반드시 반영하지는 않습니다.
