Rust와 Z3로 루프 없는 프로그램 합성하기

Synthesizing Loop-Free Programs with Rust and Z3 (2020)

프로그램 합성은 주어진 명세를 만족하는 프로그램을 자동으로 찾는 기술이다. 이 글에서는 Gulwani 등의 논문을 바탕으로 반례 기반 반복 합성(CEGIS)을 사용해 루프 없는 컴포넌트 기반 프로그램을 합성하는 방법을 설명하고, Rust와 Z3 솔버로 구현한 과정을 공유한다. 필자는 프로그램 합성에 익숙하지 않은 독자들이 개념을 이해할 수 있도록 많은 예제와 함께 논문의 복잡한 논리식을 풀어서 설명한다. 또한 이미 익숙한 독자들에게는 구현의 성능 문제를 진단하는 데 도움을 구한다. 일부 어려운 벤치마크 문제에서는 합성기가 해를 찾지 못해 인내심이 바닥나기도 한다.