AI 中文总结
该研究针对加权程序构建了演绎验证框架，证明了核心命令翻译、证明规则编码及量词消去的可靠性，基于Caesar验证器的原型可验证多类定量与符号模型相关案例。
AI 中文摘要
加权程序将带保护命令扩展为带有取自半环或更一般幺半群模的轨迹权重，改变该代数可得到多种定量和符号模型的编程语法。最弱预加权语义为这些程序的推理提供了组合基础。我们提出一种基于加权断言语言和中间验证语言的演绎验证框架，其权重域是带有蕴含和共蕴含的有序结构，能让验证条件在内部表达上下界义务。我们证明了核心命令的可靠翻译，以及适用于过程调用和循环的各类证明规则的可复用编码。为促进自动化，我们证明了断言语言量词消去过程的可靠性。在Caesar验证器中的原型，对概率队列成本、带循环依赖的递归数据库来源、任意规模网络的 clearance 边界，以及比较并交换计数器无锁性的形式语言推理等案例研究进行了检查。
英文摘要
Weighted programs extend guarded commands with trace weights drawn from a semiring, or more generally a monoid-module. Varying this algebra gives one programmatic syntax for a variety of quantitative and symbolic models. Weakest-preweighting semantics provides a compositional basis for reasoning about those programs. We present a deductive verification framework based on a weighted assertion language and an intermediate verification language. Its weight domains are ordered structures with implication and coimplication, which let verification conditions express lower- and upper-bound obligations internally. We prove sound translations of core commands and reusable encodings for various proof rules applying to procedure calls and loops. To facilitate automation, we prove soundness of a quantifier elimination procedure for our assertion language. A prototype in the Caesar verifier checks case studies for probabilistic queueing costs, recursive database provenance with cyclic dependencies, clearance bounds for networks of arbitrary size, and formal-language reasoning about lock-freedom of a compare-and-swap counter.
