허충길 교수와 이준영 박사과정생이 마이크로소프트연구소 및 유타대학교와 공동으로 개발한 LLVM 컴파일러 최적화 자동 검증 프레임워크 Alive2가 프로그래밍 언어 분야 최우수 학술대회인 PLDI 2021 (The 42th ACM SIGPLAN International Conference on Programming Language Design and Implementation)에서 최우수 논문상 (Distinguished Paper Award)을 수상하였다.

올해 6월 온라인으로 개최되는 PLDI 2021에는 총 87편의 논문이 채택되었으며, 최우수 논문상은 그 중 8편의 논문에 수여되었다.

Alive2 프레임워크는 컴파일러 실행 중 생성된 최적화 전후 프로그램들의 실행의미 및 이들의 동등함을 수식으로 표현한 후, 마이크로소프트의 자동수식검증기(SMT solver)인 Z3를 사용해 최적화의 올바름을 보이거나, 그렇지 않으면 오류를 찾아낸다. 이때 핵심기술은 프로그램의 복잡한 실행의미를 SMT solver가 쉽게 풀 수 있는 형태로 효율적으로 표현하는 것이다. SMT solver는 수학적으로 엄밀하게 수식의 참/거짓을 체크하기 때문에, Alive2는 오탐(False Alarm)이 거의 없고 테스팅으로는 찾을 수 없는 오류들을 찾아낼 수 있다.

Alive2는 지금까지 테스팅으로서는 발견할 수 없었던 수십개의 컴파일러 버그를 발견하였으며, 기존에 발견되지 않았던 LLVM 중간 언어 명세의 문제 또한 새로 발견하였다. 논문 리뷰 과정에서는 해당 기여의 중요성을 인정받아 네 명의 심사위원 전원으로부터 최고 점수인 Strong Accept 평가를 받았다.

Alive2의 온라인 서비스(https://alive2.llvm.org) 는 현재 LLVM 커뮤니티의 코드 리뷰 단계에서 개발자들에 의해 활발하게 사용되고 있다.

"Alive2: Bounded Translation Validation for LLVM.", Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr.