Caesar: 확률적 프로그램 (Probabilistic Programs)을 위한 연역적 검증기 (Deductive Verifier)

Caesar는 확률적 프로그램 (Probabilistic Programs)을 위한 연역적 검증기 (Deductive Verifier)입니다. 그 핵심에는 실수 값 논리 (Real-valued logic)인 HeyLo를 기반으로 하는 정량적 중간 검증 언어 (Quantitative intermediate verification language)인 HeyVL이 자리 잡고 있습니다. HeyVL을 통해 사용자는 확률적 프로그램, 그 사양 (Specifications), 그리고 증명 규칙 (Proof rules)을 프로그래밍 언어 스타일로 표현할 수 있어, 새로운 증명 규칙을 검증기에 쉽게 통합할 수 있습니다. Caesar는 HeyVL 프로그램을 검증 조건 (Verification conditions)으로 변환하며, 이는 Z3 SMT solver를 사용하여 확인됩니다. 또한 HeyVL의 일부 하위 집합에 대해 확률적 모델 체킹 (Probabilistic model checking)에 기반한 백엔드 (Backend)를 포함하고 있습니다. 본 논문에서는 Caesar의 5년간의 개발 결과를 보고하며, 주요 특징과 아키텍처 (Architecture)를 강조합니다. 특히 추가적인 증명 규칙, 모델 체킹 백엔드, 그리고 개선된 진단 (Diagnostics) 기능과 같은 최근의 개선 사항들을 설명합니다.