실행 파일에 분석을 포함하기
컴파일 패스가 값의 계산을 추적하는 호출을 삽입하고 런타임이 기호식을 처리한다. 실행 중에는 원래 연산과 함께 분기의 조건을 추적한다. SymCC는 현재 구체 실행 경로를 따라가며 다른 경로로 진입할 입력을 찾는 방식으로 동작한다.
입력을 반복해서 탐색하기
생성된 테스트 입력을 다시 실행하거나 퍼저와 결합해 분석을 이어갈 수 있다. 표준 입력 또는 지정한 파일의 내용을 기호 입력으로 다룬다. 어떤 데이터를 기호화했는지에 따라 해결기에 전달되는 조건과 생성되는 입력이 달라진다.
완전한 증명과의 차이
QSYM 백엔드는 속도를 위해 경로를 가지치기하며 일부 라이브러리 함수의 기호 처리는 불완전할 수 있다. 따라서 입력이 생성되지 않았다고 모든 경로가 안전하다고 결론 내리면 안 된다. 검사 환경과 지원 함수, 백엔드를 함께 확인한다.