프로그램과 속성 입력
입력 파일에는 Lustre 코드와 항상 성립해야 할 성질을 함께 작성한다. 속성이 깨지는 경우에는 이를 보여 주는 입력 순서를 얻을 수 있다. 분석 대상은 주어진 프로그램과 속성의 조합이므로 입력 모델의 가정도 결과와 함께 해석한다.
여러 엔진을 사용하는 이유
한정 모델 검사, k-귀납법, 불변식 생성과 IC3 계열 기법 등이 협력한다. 오류를 빨리 찾는 데 유리한 방법과 전체 성질을 증명하는 데 필요한 방법의 역할이 다르다. 분석 중에도 발견한 반례와 증명된 속성을 점진적으로 출력한다.
구성에 따른 의미 차이
BMC만 실행하면 속성의 일반적 유효성을 증명할 수 없다. 반대로 귀납 엔진만 선택하는 구성도 필요한 결과를 내지 못할 수 있다. 엔진 조합, 시간 제한, SMT 해결기를 함께 기록하고 종료 이유와 각 속성의 판정을 구분해 확인한다.