입력을 기호로 다루기
일반 실행은 구체적인 입력값으로 연산하지만 기호 실행은 가능한 값을 나타내는 표현을 사용한다. 분기에서는 각 방향이 가능한 조건을 따로 유지하며 실행 경로를 탐색한다.
경로 조건에서 입력 얻기
오류에 도달하거나 경로가 끝나면 그동안 쌓인 조건을 풀어 구체적인 입력을 만든다. 결정적인 실행 조건에서는 이 입력을 원래 프로그램에 넣어 같은 경로와 오류를 재현할 수 있다.
상태와 제약의 관리
많은 실행 경로와 외부 환경의 처리는 기호 실행의 주요 어려움이다. KLEE는 상태를 작게 표현하고 제약 풀기를 최적화하며 탐색 휴리스틱을 사용하도록 설계됐다.
시스템 프로그램의 평가
초기 연구는 GNU Coreutils와 BusyBox 등의 도구에서 시험 생성과 오류 발견을 평가했다. 높은 코드 도달 범위뿐 아니라 기능이 같다고 여긴 도구 사이의 결과 차이도 조사했다.