분석을 조립하는 구조
코드를 읽는 작업과 실제 검증 알고리즘을 분리한다. 앞 단계가 만든 표현을 뒤 단계가 받아 처리하므로 여러 분석 방식을 같은 기반 위에서 구성할 수 있다. Ultimate 전체를 하나의 고정된 검사 알고리즘으로 이해하면 차이를 놓치기 쉽다.
서로 다른 검증 방식
Automizer는 실행 경로에 대한 불가능성 증명을 더 넓은 경로 집합으로 일반화한다. Taipan은 추상 해석으로 경로 프로그램의 반복 불변식을 찾고, 필요한 경우 경로 추상화를 활용한다. 선택한 도구가 사용하는 원리에 따라 분석의 진행과 결과 해석이 달라진다.
명세와 구성의 역할
검증할 프로그램만 준비한다고 모든 성질이 자동으로 검사되는 것은 아니다. 어떤 속성을 확인할지 정하고 그 목적에 맞는 도구 체인을 선택해야 한다. 실행 결과를 비교할 때도 입력과 명세, 사용한 구성을 함께 맞춘다.
관련 문서
CPAchecker / Boogie / IKOS / SeaHorn