Static Symbolic Execution

symbex라고도 불리는 기호 실행(symbolic execution) 은 프로그램 상태와 관련한 메타데이터 정보를 추적해 프로그램 상태(program state)가 어떻게 변화되며 다른 프로그램 상태에 어떻게 도달할 수 있는지 추론할 수 있다. 기호 실행은 프로그램의 상태를 논리적인 수식으로 표현해 프로그램 동작에 대해 결과를 추론한다. 기호 실행은 효과적인 기법이지만 규모 가변성(scalability) 문제가 있기 때문에 사용 시 주의해야 한다.