프로그램의 제약을 논리로
분석 도구는 연산과 분기 조건을 식으로 만들어 특정 상태가 가능한지 물을 수 있다. STP는 이때 생성한 비트 수준 제약 등을 처리한다. 임의의 소스를 직접 실행하는 도구와 역할이 다르다. 비트 폭과 부호 및 배열의 의미를 원래 구현과 맞춰야 결과를 코드에 적용할 수 있다.
SAT 백엔드와 빌드
논리 제약을 푸는 과정에 SAT solver를 사용하며 빌드에 포함한 백엔드 중 실행 방식을 선택할 수 있다. 어떤 기능과 백엔드를 포함했는지에 따라 설정의 유효 범위가 다르다. 실행 인자만 바꿨다고 설치되지 않은 구성 요소까지 준비되는 것은 아니다. 재현할 때는 실제 빌드와 선택 옵션을 함께 기록한다.
입력 형식과 결과 해석
SMT-LIB2 파일이나 표준 입력으로 질의를 전달하고 라이브러리 API로도 연결할 수 있다. 지원하는 논리와 입력 형식의 범위를 확인한다. 만족하는 모델과 만족 불가능한 판정 및 제한으로 끝내지 못한 결과를 구분한다. 모델 값이 나왔다면 핵심 변수와 보조 변수를 나누어 원래 문제의 조건을 실제로 만족하는지 살핀다.