Alt-Ergo

يُستخدم برنامج Alt-Ergo ، وهو برنامج حل آلي للمعادلات الرياضية ، بشكل أساسي في التحقق الرسمي من البرامج . ويعمل البرنامج وفق مبدأ قابلية الإرضاء المعياري للنظريات (SMT). وقد تولى تطويره باحثون من جامعة باريس الجنوبية ، ومختبر أبحاث المعلوماتية، ومعهد Inria Saclay Ile-de-France، والمركز الوطني للبحث العلمي (CNRS ). ومنذ عام 2013، تتولى شركة OCamlPro إدارة المشروع والإشراف عليه. ^{[ 1 ]} وهو مُرخص بموجب رخصة البرمجيات الحرة والمفتوحة المصدر CeCILL-C.

تعتمد العديد من منصات التحقق على Alt-Ergo:

• Why3 ، وهي منصة للتحقق من البرامج الاستنتاجية، تستخدم Alt-Ergo كأداة إثبات رئيسية ^{[ 2 ].}
• CAVEAT، وهو مُدقِّق من الفئة C طوّرته CEA واستخدمته شركة إيرباص؛ تم تضمين Alt-Ergo في تأهيل DO-178C لإحدى طائراتها
• يستخدم Frama-C ، وهو إطار عمل لتحليل كود C، Alt-Ergo في إضافات Jessie و WP (المخصصة للتحقق الاستنتاجي من البرامج ).
• يستخدم برنامج SPARK تقنية Alt-Ergo (التي تعمل خلف GNATprove) لأتمتة التحقق من بعض التأكيدات في Spark 2014
• يمكن لـ Atelier-B استخدام Alt-Ergo بدلاً من أداة التحقق الرئيسية الخاصة به (مما يرفع نسبة النجاح من 84% إلى 98% في معايير مشروع ANR Bware ).
• يمكن لإطار عمل Rodin ، وهو إطار عمل B-method طورته شركة Systerel، استخدام Alt-Ergo كخلفية.
• كيوبيكل ، أداة مفتوحة المصدر للتحقق من خصائص السلامة لأنظمة الانتقال القائمة على المصفوفات
• EasyCrypt ، مجموعة أدوات للاستدلال حول الخصائص العلائقية للحسابات الاحتمالية باستخدام التعليمات البرمجية المعادية
• BWARE ^{[ 3 ]}
• الكافيين ^{[ 3 ]}
• FUI Hi-Lite ^{[ 3 ]}
• ديسرت ^{[ 3 ]}
• ADT Alt-Ergo ^{[ 3 ]}
• A3PAT ^{[ 3 ]}

• التحقق الرسمي
• برنامج إثبات النظريات Z3

• الموقع الرسمي ، OcamlPro
• Alt-Ergo في LRI