شهادة المطابقة

CompCert هو مُصرّف مُحسِّن تم التحقق منه رسميًا لمجموعة فرعية كبيرة من لهجة لغة البرمجة C ، المسماة C99 والمعروفة باسم Clight. اعتبارًا من عام 2018يدعم CompCert معمارية المعالجات ARM و PowerPC و RISC-V و x86 و x86-64 . ^{[ 3 ] [ 4 ]} بدأ المشروع رسميًا عام 2005 بقيادة كزافييه ليروي ، بتمويل من الوكالة الوطنية الفرنسية للبحث العلمي (ANR) والمعهد الفرنسي لأبحاث علوم الحاسوب والأتمتة (INRIA). يُحدد المُصرّف ويُبرمج ويُثبت في برنامج مساعد الإثبات Rocq . يُستخدم CompCert لبرمجة الأنظمة المُدمجة التي تتطلب موثوقية عالية . غالبًا ما يكون أداء الكود المُولّد قريبًا من أداء مجموعة مُصرّفات GNU (GCC) الإصدار 3، عند مستوى التحسين -O1، ودائمًا ما يكون أفضل من أداء GCC بدون أي تحسينات. ^{[ 5 ]}

منذ عام ٢٠١٥، تُقدّم AbsInt تراخيص تجارية، ^{[ ٦ ]} وتُوفّر الدعم والصيانة، وتُساهم في تطوير الأداة. أما CompCert، فيتم إصداره بموجب ترخيص غير تجاري، وبالتالي فهو ليس برنامجًا مجانيًا ، على الرغم من أن بعض ملفاته المصدرية مرخصة بترخيص مزدوج بموجب رخصة جنو العمومية الصغرى الإصدار ٢.١ أو أحدث، أو متاحة بموجب شروط تراخيص أخرى. ^{[ ٢ ]}

حصل كزافييه ليروي وفريق تطوير CompCert على جائزة ACM لأنظمة البرمجيات لعام 2021 لتطوير CompCert، وهو أول مترجم تحسين عملي مفيد يستهدف العديد من البنى التجارية والذي يحتوي على برهان كامل تم التحقق منه آليًا على صحته .

• الموقع الرسمي
• CompCert على GitHub
• التحقق الرسمي من مترجم واقعي
• جائزة نظام البرمجيات - جوائز ACM