알트 에르고
Alt-Ergo |
 |
 | |
| 개발자 | OCamlPro |
|---|---|
| 리포지토리 | |
| 유형 | 수학적 해결사, 프로그램 검증기 |
| 웹사이트 | http://alt-ergo.lri.fr |
Alt-Ego는 프로그램 검증을 위해 특별히 고안된 수식 자동 해결사다.만족도 모듈로이론(SMT)에 근거한다.오픈소스 라이선스(Ceil-C)로 배포된다.원작자는 LRI의 실뱅 콘촌과 이블린 콘테장이었으나 현재는 OCamlPro에서 개발, 유지되고 있다.
기술
설계 선택사항
대부분의 SMT 해결사들과는 달리 Alt-Ego는 혼전 다형성이 있는 특정 입력 언어를 사용한다.이것은 정량화된 공리의 수와 문제의 복잡성을 줄이는 데 도움이 된다.SMT-LIB 2 언어도 부분적으로 지원하지만 SMT 파일에서는 성능이 떨어진다.
주성분
Alt-Ego의 핵심은 DFS 기반 SAT 해결사, E-Matching에 기반한 정량자 인스턴스화 엔진, 그리고 일련의 내장 이론에 대한 의사결정 절차의 조합의 세 부분으로 이루어져 있다.
빌트인
Alt-Ego는 다음과 같은 이론에 대해 (semi-)결정 절차를 구현한다.
- 공허한 이론
- 선형 정수 산술
- 선형적 이성적 산술
- 비선형 산술
- 부동 소수점 산술
- 다형 배열
- 열거된 데이터 유형
- AC 기호
- 데이터 유형을 기록하다
산업용
Alt-Ego 위에 다음과 같은 몇 가지 검증 플랫폼이 구축되어 있다.
- 연역 프로그램 검증을 위한 플랫폼인 Why3는 Alt-Ego를 주요 프로베러로 사용한다.
- CEA에 의해 개발되고 에어버스에서 사용되는 C-검증기인 COVERAT; Alt-Ego는 항공기 중 하나의 DO-178C 자격에 포함되었다.
- C-코드를 분석하는 프레임워크인 Frama-C는 제시와 WP 플러그인의 Alt-Ego를 사용한다("고교 프로그램 검증" 전용).
- 스파크, Alt-Ego(GNATProve 후면)를 사용하여 스파크 2014의 일부 주장에 대한 검증을 자동화함.
- 아틀리에-B는 메인 프로베러 대신 Alt-Ego를 사용할 수 있다(ANR Bware 프로젝트 벤치마크에서 84%에서 98%로 성공률 증가).
- 로댕은 시스테렐이 개발한 B-method 프레임워크로 Alt-Ego를 백엔드로 사용할 수 있다.
- 어레이 기반 전환 시스템의 안전 특성을 검증하기 위한 오픈 소스 모델 체커인 큐비클.
- EasyCrypt, 대립 코드와의 확률론적 계산의 관계적 특성에 대한 추론을 위한 도구 모음입니다.
