예언 기반 메시지 전달 프로그램의 자동 검증 (Prophecy-Based Automated Verification of

우리는 검증 문제를 제약된 Horn 절 (Constrained Horn Clause, CHC) 풀이 문제로 환원함으로써, 메시지 전달 병렬 프로그램 (message-passing concurrent programs)의 기능적 정확성 (functional correctness)을 검증하기 위한 완전 자동화된 방법을 제안합니다. RustHorn의 예언 기반 (prophecy-based) 기술에서 영감을 받아, 우리는 각 송신 채널 (sender channel)을 향후 해당 채널을 통해 전송될 값들의 목록으로 표현하며, 이를 통해 CHC 내에서 송신 및 수신 스레드 (sender and receiver threads)의 모듈식 인코딩 (modular encoding)을 가능하게 합니다. 서로 다른 채널 간의 인과적 의존성 (causal dependencies)을 포착하기 위해, 우리는 메시지에 타임스탬프 (timestamps)를 추가로 부착합니다. 우리는 결과적인 환원이 건전성 (sound)과 완전성 (complete)을 가짐을 증명합니다: 즉, 프로그램이 어설션 실패 (assertion failures)로부터 자유할 필요충분조건은 대응하는 CHC 시스템이 충족 가능 (satisfiable)한 것입니다. 또한 우리는 Rust 스타일의 프로그램을 위한 프로토타입 검증기 (prototype verifier)를 구현하였으며, 실험을 통해 이 접근 방식의 효과를 확인하였습니다.