코드에서 검증 조건까지
주석을 단 C 프로그램을 중간 표현으로 바꾸고 검증 조건을 만든 뒤 solver로 푸는 파이프라인을 제공한다. 각 단계를 따로 실행해 생성 자료를 살펴볼 수도 있다. 프로그램을 LLVM으로 변환할 수 있다는 사실만으로 모든 언어 기능과 외부 동작을 정확하게 검증한다는 뜻은 아니다.
다른 분석의 결합
경계 있는 모델 검사와 불변식 추론 및 추상 해석을 목적에 따라 구성한다. Crab 분석을 통해 얻은 성질을 다른 검증 단계에 전달할 수 있으나 모든 기능이 기본으로 실행되지는 않는다. 레지스터만 추적하는 설정과 포인터 및 메모리 내용까지 모델링하는 설정은 정밀도가 다르므로 실제 확인한 범위를 구분한다.
결과를 읽는 방향
일반적인 단언 검증 흐름에서는 오류 위치에 도달할 수 없으면 unsat, 도달할 수 있으면 sat으로 표시한다. 표기만 보고 성공과 실패를 반대로 해석하지 않도록 질의 의미를 확인한다. 프레임워크는 바로 쓰는 완제품 분석기와 구분되며 구성 부품과 버전의 영향을 받는다. 소스와 변환 자료 및 옵션을 보존하고 반례가 실제 실행에서 나타나는지도 조사한다.