Symbolic execution이란?
Symbolic execution
프로그램 실행 시 사용되는 미지수의 값을 기호로 가정하여 프로그램을 분석하는 방법
#include <stdio.h> void main() { int x, y, z; scanf("%d", &x); scanf("%d", &y); z = x *2; if(z ==1000) { if(y > z) { printf("Nice!\n"); } else{ printf("Wrong!\n"); } } } |
■ x와 y는 미지수이므로 각각 기호로 가정
- x = α
- y = β
■ 나타날 수 있는 모든 경우
- z의 값이 1000이 아닐 경우 : (α * 2) ≠ 1000
- z의 값이 1000이고 y의 값이 z보다 작거나 같을 경우 : ((α * 2) = 1000) && β ≤ (α * 2)
- z의 값이 1000이고 y의 값이 z보다 클 경우 : ((α * 2) = 1000) && β > (α * 2)
이와 반대되는 용어로 Concrete execution이 있습니다.
Concrete execution
프로그램 실행 시 구체적인 값을 이용하여 프로그램을 분석하는 방법
#include <stdio.h>
if(1) { printf("Nice!\n"); } else { printf("Wrong!\n"); } } |
■ 1이라는 고정 값에 의해 "Nice!\n" 문구 출력
■ 프로그램을 여러 번 실행해도 실행되는 경로와 결과가 동일
참고 : https://www.lazenca.net/pages/viewpage.action?pageId=6324534