Alt-Ergo - Alt-Ergo - Wikipedia

Alt-Ergo je automatický řešič matematických vzorců, speciálně navržený pro verifikaci programu. Je to založeno na teorie uspokojivosti modulo (SMT). Je distribuován pod licencí open-source (Cecill-C). Jeho původními autory byli Sylvain Conchon a Evelyne Contejean, at LRI, ale nyní je vyvíjen a udržován na OCamlPro.

Technologie

Možnosti designu

Na rozdíl od většiny řešitelů SMT používá Alt-Ergo specifický vstupní jazyk s polymorfismus prenex. To pomáhá snižovat počet kvantifikovaných axiomů a složitost problémů. Částečně také podporuje jazyk SMT-LIB 2, ale na soubory SMT funguje méně efektivně.

Hlavní součásti

Jádro Alt-Ergo se skládá ze tří částí: SAT řešič založený na DFS, instanční modul kvantifikátorů založený na E-Matching a kombinace rozhodovacích postupů pro sadu integrovaných teorií.

Integrované teorie

Alt-Ergo implementuje (polo) rozhodovací postupy pro následující teorie:

Průmyslové použití

Na platformě Alt-Ergo je postaveno několik ověřovacích platforem:

  • Proč3, platforma pro deduktivní ověření programu, používá Alt-Ergo jako hlavní prover;
  • CAVEAT, ověřovatel C vyvinutý společností CEA a používaný společností Airbus; Alt-Ergo byl zařazen do kvalifikace DO-178C jednoho ze svých letadel;
  • Frama-C, rámec pro analýzu C-kódu, používá Alt-Ergo v zásuvných modulech Jessie a WP (vyhrazeno pro "deduktivní ověření programu");
  • JISKRA, používá Alt-Ergo (za GNATprove) k automatizaci ověřování některých tvrzení ve Sparku 2014;
  • Atelier-B může použít Alt-Ergo místo svého hlavního proveru (zvýšení úspěšnosti z 84% na 98% na Benchmarky projektu ANR Bware );
  • Rodine, rámec metody B vyvinutý společností Systerel, může používat Alt-Ergo jako back-end;
  • Kóje, open source model checker pro ověřování bezpečnostních vlastností přechodových systémů založených na poli.
  • EasyCrypt, sada nástrojů pro uvažování o relačních vlastnostech pravděpodobnostních výpočtů s kontradiktorním kódem.

Viz také

externí odkazy