시스템 환경 속 분석
한 함수만 따로 떼어 모델링하기보다 소프트웨어 스택 안에서 관심 있는 부분의 동작을 살필 수 있다. 모듈식 라이브러리로 가상 머신에 분석 능력을 제공한다. 지원하는 아키텍처와 운영체제 및 이미지 구성을 확인해야 하며 임의 환경이 준비 없이 그대로 분석되는 것은 아니다.
경로를 선택하는 이유
기호 실행은 분기마다 가능한 경로가 늘어나 비용이 커질 수 있다. 선택기는 관심 구성 요소에 탐색을 집중시키고 분석기는 각 경로에서 원하는 성질을 확인한다. 무엇을 구체적으로 실행하고 무엇을 기호적으로 다뤘는지가 결과의 범위를 결정한다. 선택하지 않은 경로의 성질까지 확인했다고 해석하지 않는다.
플러그인과 결과 재현
프로그램 모니터와 실행 추적 및 사용자 정의 플러그인 등으로 분석을 확장할 수 있다. 오류 처리 코드의 동작이나 여러 실행 경로의 차이를 조사하는 데 활용한다. 이미지와 프로그램 및 플러그인 설정을 함께 보존해야 결과를 재현하기 쉽다. 제한된 탐색에서 문제가 없었다는 사실과 전체 시스템의 안전성 증명은 구분한다.