컴파일러가 넣는 오류 줄이기
소스 프로그램을 분석했더라도 번역 과정에서 의미가 달라지면 실행 결과가 어긋날 수 있다. CompCert는 컴파일 변환과 소스 의미의 관계를 기계 검사된 증명으로 다룬다. 이를 통해 소스 수준의 형식 분석과 실행 코드 사이의 연결을 강화한다.
응용 프로그램의 정확성과 구분
올바른 컴파일은 원래 프로그램이 요구 사항을 만족한다는 주장과 다르다. 소스에 논리 오류가 있다면 컴파일러의 의미 보존만으로 해결되지 않는다. 프로그램이 사용하는 언어 기능과 동작이 명세의 지원 범위 안에 있는지도 확인해야 한다.
실제 도구 연결
같은 C 코드라도 아키텍처와 ABI, 컴파일 설정에 따라 실행 환경이 달라진다. 검증된 변환과 외부 도구, 런타임의 경계를 구분해 사용하는 것이 중요하다. 특정 검증 결과를 적용할 때는 사용한 컴파일러 버전과 대상 구성을 함께 기록한다.
관련 문서
CakeML / Alive2 / Frama-C / Gillian 검증 플랫폼