CompCert

ผู้ประกอบการ

คอมไพเลอร์ C ที่ผ่านการตรวจสอบอย่างเป็นทางการ

ภาพรวม

Compcert C ที่ผ่านการตรวจสอบแล้วคอมไพเลอร์เป็นคอมไพเลอร์สำหรับชุดย่อยขนาดใหญ่ของภาษาการเขียนโปรแกรม C ที่สร้างรหัสสำหรับโปรเซสเซอร์ PowerPC, ARM, x86 และ RISC-V

คุณลักษณะที่แตกต่างของ Compcert คือได้รับการตรวจสอบอย่างเป็นทางการโดยใช้ผู้ช่วยพิสูจน์ COQ: รหัสแอสเซมบลีที่สร้างขึ้นนั้นรับประกันได้ว่าจะทำงานอย่างเป็นทางการตามที่กำหนดโดยความหมายของรหัสต้นแหล่ง C

สำหรับข้อมูลเพิ่มเติมเกี่ยวกับ CompCert (แพลตฟอร์มที่รองรับคุณสมบัติ C ที่รองรับคำแนะนำการติดตั้งโดยใช้คอมไพเลอร์ ฯลฯ ) โปรดดูเว็บไซต์และโดยเฉพาะอย่างยิ่งคู่มือผู้ใช้

ใบอนุญาต

Compcert ไม่ใช่ซอฟต์แวร์ฟรี การเปิดตัวที่ไม่ใช่เชิงพาณิชย์นี้สามารถใช้สำหรับการประเมินผลการวิจัยการศึกษาและวัตถุประสงค์ส่วนตัวเท่านั้น Compcert เวอร์ชันเชิงพาณิชย์โดยไม่มีข้อ จำกัด นี้และด้วยการสนับสนุนอย่างมืออาชีพและคุณสมบัติพิเศษสามารถซื้อได้จาก Absint ดู LICENSE ไฟล์สำหรับข้อมูลเพิ่มเติม

ลิขสิทธิ์

คอมไพเลอร์ที่ผ่านการตรวจสอบแล้ว Compcert เป็น Institut National de recherche en Informatique et en Automatique (Inria) และ Absint Angewandte Informatik GmbH

ติดต่อ

การอภิปรายทั่วไปเกี่ยวกับ Compcert เกิดขึ้นในรายการจดหมายสมัครงาน [email protected]

สำหรับข้อสงสัยเกี่ยวกับ Compcert เวอร์ชันเชิงพาณิชย์กรุณาติดต่อ [email protected]