jayhorn
version 0.7
| ผู้เชี่ยวชาญ | ||||
|---|---|---|---|---|
| จ้อง |
คำสั่ง Java และ Horn
Jayhorn เป็นเครื่องมือตรวจสอบแบบจำลองซอฟต์แวร์สำหรับ Java Jayhorn พยายามหาหลักฐานว่ารัฐที่ไม่ดีบางอย่างในโปรแกรม Java ไม่สามารถเข้าถึงได้ สถานะที่ไม่ดีเหล่านี้ถูกระบุโดยการเพิ่มการยืนยันรันไทม์ (ซึ่งอาจมีการยืนยันบางอย่างเช่นการอ้างอิงวัตถุจะต้องไม่เป็นโมฆะก่อนที่จะเข้าถึง)
Jayhorn พยายามที่จะทำผิดพลาดที่ด้านความแม่นยำนั่นคือเมื่อไม่สามารถพิสูจน์ได้ว่าการยืนยันอยู่เสมอมันจะอ้างว่าการยืนยันอาจถูกละเมิด (เรียกว่าความสมบูรณ์) Jayhorn ปัจจุบันเป็นเสียง (Modulo Bugs) สำหรับ Java ที่ใช้เธรดเดียวไม่มีการโหลดคลาสแบบไดนามิกและไม่ดำเนินการที่ซับซ้อนในการเริ่มต้นแบบคงที่
สำหรับข้อมูลเกี่ยวกับวิธีการดาวน์โหลดและเรียกใช้ 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โครงการนี้ได้ทำในจิตวิญญาณแห่งความน่าอัศจรรย์ เมื่อสร้างการวิเคราะห์โปรแกรมเชิงปฏิบัติมักจำเป็นต้องตัดมุม เพื่อที่จะเปิดเกี่ยวกับคุณสมบัติภาษาที่เราไม่สนับสนุนหรือสนับสนุนเพียงบางส่วนเท่านั้นเรากำลังแนบคำสั่ง Soundiness นี้
การวิเคราะห์ของเราไม่ได้มีการจัดการที่ดีของคุณสมบัติต่อไปนี้:
คำแถลงนี้ได้รับการผลิตด้วยเครื่องกำเนิดความน่าสะพรึงกลัวจาก Soundiness.org
Jayhorn เป็นโอเพ่นซอร์สและแจกจ่ายภายใต้ใบอนุญาต MIT
ห้องสมุดที่ใช้ใน Jayhorn รวมถึงโดยเฉพาะ:
Jayhorn ได้รับทุนบางส่วนโดย:
ความคิดเห็นการค้นพบและข้อสรุปหรือคำแนะนำใด ๆ ที่แสดงในเนื้อหานี้เป็นของผู้เขียนไม่จำเป็นต้องสะท้อนมุมมองของ AFRL, DARPA, NSF หรือสภาวิจัยสวีเดน
