구체적인 값 대신 기호 사용
입력 값을 하나씩 고정하기보다 기호로 표현하고 분기 조건과 연산의 관계를 추적한다. 실행 경로에서 얻은 논리 조건으로 안전성을 확인하거나 반례를 찾을 수 있다. 탐색하는 모델이 프로그램을 어떻게 표현했는지에 따라 결과의 의미가 달라진다. 언어 독립적이라는 말이 모든 소스를 바로 받아들인다는 뜻은 아니다.
여러 프런트엔드
LLVM과 JVM을 위한 변환 및 실행 지원이 있고 Rust에는 MIR 기반 연결이 있다. Crux 계열 도구는 시뮬레이터를 실행하고 생성된 안전 조건을 모아 검증하는 공통 절차를 제공한다. 각 입력 형식과 언어 기능의 지원 범위를 확인하고 일반 컴파일 성공과 기호 실행 지원을 구분한다.
확장과 실행 조건
Haskell에서 새 연산과 자료형을 구현해 시뮬레이터를 확장할 수 있다. 논리식 표현과 증명기 연결은 What4를 활용한다. 사용한 메모리 모델과 외부 함수 처리 및 탐색 설정이 확인 범위에 영향을 준다. 시간이 부족해 끝내지 못한 탐색과 오류가 없는 결과를 혼동하지 않고 소스와 중간 자료 및 도구 버전을 함께 유지한다.