코드를 조건식으로 바꾸기
입력값을 몇 개 골라 실행하는 대신, 분기와 연산을 만족해야 하는 조건으로 표현한다. 배열 범위 초과나 잘못된 포인터 접근에 도달할 수 있는지 해결기에 묻는다. 오류가 발견되면 그 조건에 맞는 실행 흐름을 분석할 수 있다.
반복과 스레드 다루기
반복문을 유한하게 펼쳐 검사하는 방식과 점진적으로 범위를 늘리는 방식이 있다. pthread 기반 동시성 검사에서는 스레드 실행 순서도 고려한다. 교착이나 경쟁 상태 등은 검사 옵션과 지원 조건을 구분해서 설정한다.
결과의 범위
일정 깊이에서 오류가 없다는 결과와 전체 실행에 대한 증명은 의미가 다르다. 귀납법의 성공 여부, 반복 전개 한계, 선택한 속성을 함께 확인해야 한다. 프런트엔드마다 지원하는 언어 기능도 같지 않다.
관련 문서
CPAchecker / SeaHorn / Bitwuzla / Yices