무상으로 제공되는 정확하고 완전한 심볼릭 실행 (Symbolic Execution)

심볼릭 실행 (Symbolic execution)은 프로그램 분석을 위한 강력한 기술입니다. 그러나 심볼릭 실행의 근간이 되는 형식적 의미론 (formal semantics)은 종종 임시방편적 (ad-hoc)으로 개발되며, 프로그래밍 언어의 구체적 의미론 (concrete semantics)과 분리되어 있습니다. 이 문제를 극복하기 위해, 우리는 구체적 의미론과 심볼릭 의미론을 동시에 지정할 수 있게 해주는 규칙 형식인 symbolic SOS를 소개합니다. 우리는 symbolic SOS로부터 생성된 심볼릭 의미론 (symbolic semantics)이 대응하는 구체적 의미론에 대해 정확성 (correctness)과 완전성 (completeness)을 모두 갖추고 있음을 증명합니다. 이 접근 방식은 소스 언어의 대수적 시그니처 (algebraic signature)에만 의존하므로 언어 독립적 (language-independent)입니다.