アルトエルゴ

Alt-Ergo は、数式の自動ソルバーであり、主に形式的なプログラム検証に使用されます。理論による充足可能性(SMT)の原理に基づいて動作します。開発は、パリ・シュッド大学、情報科学研究所、Inria Saclay Ile-de-France、およびCNRSの研究者によって行われました。2013 年以降、プロジェクトの管理と監督は OCamlPro 社によって行われています。^{[ 1 ]}フリーでオープンソースのソフトウェアCeCILL-C ライセンスの下でリリースされています。

Alt-Ergoを基盤とした検証プラットフォームは複数存在する。

• 演繹的プログラム検証プラットフォームであるWhy3は、メインの証明器としてAlt-Ergoを使用しています^{[ 2 ]。}
• CAVEATはCEAが開発し、エアバスが使用しているC検証ツールです。Alt-Ergoは、同社の航空機のDO-178C認証に含まれています。
• C言語コードを分析するためのフレームワークであるFrama-Cは、JessieおよびWPプラグイン（演繹的プログラム検証専用）においてAlt-Ergoを使用しています。
• Spark は、Alt-Ergo (GNATprove の背後) を使用して、Spark 2014 における一部のアサーションの検証を自動化しています。
• Atelier-Bは、メインの検証装置の代わりにAlt-Ergoを使用できる（ANR Bwareプロジェクトのベンチマークにおける成功率が84%から98%に向上する）。
• Systerelが開発したBメソッドフレームワークであるRodinは、バックエンドとしてAlt-Ergoを使用できる。
• Cubicleは、配列ベースの遷移システムの安全性を検証するためのオープンソースのモデルチェッカーです。
• EasyCryptは、敵対的コードを用いた確率的計算の関係特性について推論するためのツールセットです。
• BWARE ^{[ 3 ]}
• カフェイン^{[ 3 ]}
• FUIハイライト^{[ 3 ]}
• 証明^{[ 3 ]}
• ADT Alt-Ergo ^{[ 3 ]}
• A3PAT ^{[ 3 ]}

• 形式検証
• Z3定理証明器

• 公式サイト、OcamlPro
• LRIのAlt-Ergo