논리식에 해가 있는가
프로그램이나 시스템에서 나온 조건을 논리식으로 표현하면, 그 조건을 동시에 만족하는 값이 있는지 물을 수 있다. OpenSMT는 이런 질의를 처리하는 해결기다. 원래 프로그램 전체를 직접 이해하는 도구와 달리 입력으로 전달된 식과 선택한 논리를 다룬다.
지원 논리의 범위
양화사 없는 미해석 함수, 정수와 실수의 선형 산술, 차분 논리, 배열에 관한 논리 등을 지원한다. 산술을 지원한다는 설명이 모든 비선형 문제까지 처리한다는 뜻은 아니다. 입력이 어느 논리 조각에 해당하는지 구분해야 한다.
검증 도구의 구성 요소
명령행 실행 외에 API로 다른 분석기에 연결할 수 있다. 실제 검증 결과는 해결기뿐 아니라 조건식을 만드는 프런트엔드에도 의존한다. 빌드할 실행 파일과 라이브러리를 선택할 수 있으므로 연동 시 필요한 구성 요소가 포함되었는지 확인한다.
관련 문서
Z3 / Yices / Kind 2 / Sally 모델 검사기