반복을 펼친 프로그램
반복문을 정한 깊이까지 펼친 뒤 단언이 붙은 프로그램을 수식으로 변환한다. 이 수식을 결정 절차에 전달해 위반 가능한 실행을 찾는다.
반례와 범위 안의 안전성
수식을 만족하는 해가 있으면 단언을 위반하는 실행이 존재한다. 안전하다는 결과도 주어진 한계 안에서의 판단이므로 반복 범위를 어떻게 정했는지가 의미에 포함된다.
메모리와 사용자 속성
배열 경계와 포인터의 안전한 사용, 여러 종류의 정의되지 않은 동작 및 사용자가 지정한 단언을 검사한다. 프로그램이 지켜야 할 조건을 명시해 확인하는 도구다.
다양한 분석의 활용
오류 찾기와 속성 검사 외에 시험 입력 생성과 동등성 검사, 프로그램 합성 등에도 활용할 수 있다. 목적에 따라 어떤 조건을 수식으로 표현하고 검사하는지가 달라진다.
관련 문서
KLEE / UndefinedBehaviorSanitizer / Csmith / 소프트웨어 테스트 / 컴파일러 / 프로그래밍