Towards a Deductive Verification Infrastructure for Weighted Programming

arXiv (Cornell University)

Abstract

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.

Authors 4

1. Emma Ahrens Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Germany

2. Samuel Rode Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Germany

3. Philipp Schröer Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Germany

4. Joost-Pieter Katoen Aachen

   RWTH Aachen University

   Affiliation as printed

   RWTH Aachen University , Aachen , Germany;

   RWTH Aachen University , Germany