해결기에서 보간까지
SMT 판정은 주어진 조건들이 함께 성립할 수 있는지 묻는다. 보간식은 서로 양립할 수 없는 식 사이의 공통 정보를 표현하는 데 활용된다. 상위 검증 알고리즘은 이 정보를 이용할 수 있지만 보간식 자체가 전체 프로그램의 증명은 아니다.
논리 이론별 차이
미해석 함수와 선형 산술, 비트벡터, 배열과 자료형 등을 지원한다. 양화사 지원과 보간 지원은 모든 이론에서 같지 않다. 특히 자료형과 양화사 없는 조각의 조건을 구분해 실제 질의에 필요한 기능이 있는지 확인한다.
분석 도구와 연동
Java 환경에서 실행하고 표준 형식의 질의를 전달할 수 있다. 같은 형식의 파일이라도 사용하는 이론과 옵션에 따라 처리 범위가 달라진다. 모델 검사기에서 활용할 때는 해결기의 버전과 보간에 필요한 구성을 함께 기록한다.
관련 문서
MathSAT / OpenSMT / Kind 2 / Ultimate 프로그램 분석