오류에 도달하는 실행 찾기
오류가 없다는 증명을 직접 만드는 관점과 오류를 일으키는 실행이 존재하는지 묻는 관점은 다르다. Corral은 제어 흐름과 논리식을 함께 표현한 프로그램에서 특정 위치의 도달 가능성을 조사한다. 초기 상태와 오류 위치 및 연산의 의미를 어떻게 모델링했는지가 결과를 결정한다.
필요한 호출과 추상화
도구의 알고리즘은 필요한 절차 호출을 펼치고 추상화한 분석을 점진적으로 정교하게 만드는 방식을 사용한다. 모든 소스 경로를 구체적으로 실행하는 검사와 구분된다. 분석이 복잡해 끝나지 않은 상태를 오류가 없다는 결과로 받아들이지 않으며 모델과 설정의 범위 안에서 결과를 해석한다.
검증 체계에서의 역할
Boogie 모델을 만드는 다른 도구 뒤에서 검증 절차를 맡을 수 있으며 SMACK도 Corral을 활용한다. 임의의 C나 Rust 소스를 바로 입력하는 도구와는 다르다. 원래 구현과 중간 모델의 관계를 확인하고 변환 도구 및 solver 버전을 함께 보존한다. 오류 경로가 보고되면 그 경로가 실제 구현에서 재현되는지도 조사한다.