확인할 성질을 먼저 선택
검사할 오류 지점을 기준으로 프로그램을 슬라이싱하면 해당 성질과 관련 없는 부분을 줄일 수 있다. 이 과정에서 다른 종류의 오류가 있는 코드가 빠질 수도 있다. 따라서 단언 위반을 찾는 설정의 성공을 메모리 안전성까지 확인한 결과로 받아들이면 안 된다. 어떤 성질을 대상으로 분석했는지 분명히 기록한다.
분석 도구의 조합
기본적으로 KLEE를 사용하며 다른 검증기를 연결하는 구성도 제공한다. 구성 요소는 별도 프로그램이나 LLVM 패스 등으로 나뉘어 있다. 일부 백엔드 연동은 실험적으로 안내되므로 이름이 목록에 있다는 사실만으로 모든 기능이 같은 수준에서 동작한다고 가정하지 않는다. 실제 빌드와 실행 설정을 확인한다.
오류 추적과 배포 상태
발견한 오류 경로를 표시하고 일부 경우에는 실제로 실행할 수 있는 증거를 생성한다. 이를 이용해 변환 전 프로그램에서 문제를 재현하는지 조사할 수 있다. 공식 안내는 오래된 배포와 갱신되지 않은 컨테이너에 대한 주의도 설명한다. 사용할 아카이브와 구성 요소 및 LLVM 버전을 맞추고 현재 환경에서 검사 과정을 재현한다.