코드와 명세를 함께 준비
전처리한 C 코드를 입력하거나 도구의 전처리 기능을 사용할 수 있다. 어떤 오류 위치나 단언을 검사할지도 명세와 설정에 따라 정한다. 소스를 읽었다는 사실만으로 필요한 모든 성질을 자동으로 확인하는 것은 아니다. 매크로와 외부 함수 및 여러 파일의 연결이 분석 모델과 맞는지 확인한다.
분석 구성과 의존성
술어 분석이나 귀납법 등 목적에 맞는 구성을 선택할 수 있다. 각 구성에서 필요한 solver와 지원 플랫폼은 다를 수 있다. 도구의 라이선스와 함께 배포된 solver의 사용 조건도 별도로 확인한다. 실행 환경이 준비되었다고 모든 구성이 같은 방식으로 작동한다고 가정하지 않는다.
판정과 반례 확인
결과를 HTML 보고서와 오류 경로 및 변수 배정 등으로 조사할 수 있다. 일부 구성에서는 재현용 검사 하네스도 만든다. 위반 증거를 실행 검사로 확인하는 기능은 원래 소스와 명세 및 증거 자료가 서로 맞아야 한다. 반례 정보가 부족해 검증하지 못한 결과와 위반이 재현된 결과를 구분하고 입력 및 옵션을 보존한다.