허충길 교수 연구진에서 새로 개발한 분할 컴파일 검증 기술이 세계 유일의 검증된 상용 컴파일러 컴프서트(CompCert)에 도입되었다.

최근 발표된 컴프서트의 최신 버전(CompCert 2.7)에서는 가장 큰 개선으로 허충길 교수 연구진의 연구 성과 ("Lightweight verification of separate compilation", POPL 2016)를 적용한 점을 꼽았다.

컴프서트는 프랑스의 INRIA 연구소에서 개발하고 독일 AbsInt 사에서 상용화한 세계 유일의 검증된 상용 컴파일러로서, 항공기 자동항법 시스템과 같이 안전이 필수인 시스템 분야에 활용이 기대되고 있다.

새로 적용된 기술은 여러 개의 파일로 작성된 소스프로그램을 파일별로 따로 컴파일 하는 경우에도 컴파일 오류가 없음을 검증한 것이다. 기존에는 전체 소스 프로그램이 한 파일로 작성되었을 경우에만 컴파일러 무오류성이 검증되었다. 이번에 허충길 교수팀이 분할 컴파일로 증명을 확장하는과정에서 실제 컴프서트의 분할 컴파일 관련 2개의 오류를 발견하고 이를 수정 후 검증을 완료했다.

이 소식 관련 보다 자세한 내용은 아래의 링크를 통해 확인할 수 있다.

컴프서트 공식 사이트 http://compcert.inria.fr/, https://www.absint.com/compcert/
컴프서트 2.7 Change Log http://compcert.inria.fr/release/Changelog
검증 기술 소개 페이지 http://sf.snu.ac.kr/sepcompcert/