Caesar is a deductive verifier for probabilistic programs. At its core lies HeyVL, a quantitative intermediate verification language based on the real-valued logic HeyLo. HeyVL allows users to express a probabilistic program, its specifications, and proof rules in a programming-language style, so that new proof rules can be easily integrated into the verifier. Caesar translates HeyVL programs into verification conditions, which are then checked using the Z3 SMT solver. It also includes a backend based on probabilistic model checking for a subset of HeyVL. We report on the results of five years of development of Caesar, highlighting its main features and architecture. In particular, we describe recent improvements such as additional proof rules, a model-checking backend, and better diagnostics.

翻译：Caesar 是一款面向概率程序的演绎验证器。其核心是 HeyVL——一种基于实值逻辑 HeyLo 的定量中间验证语言。HeyVL 允许用户以编程语言风格表达概率程序、其规约及证明规则，从而可将新证明规则轻松集成至验证器中。Caesar 将 HeyVL 程序转换为验证条件，并通过 Z3 SMT 求解器进行检验。此外，它还包含一个基于概率模型检验的 HeyVL 子集后端。本文报告了 Caesar 五年开发历程的成果，重点介绍其主要特性与架构，特别描述近期改进，如新增证明规则、模型检验后端以及更优的诊断功能。