A Weakest Precondition Calculus for Programs and Linear Temporal Specifications

TL;DR

This paper addresses the challenge of verifying temporal properties within auto-active, imperative programs by marrying a weakest precondition calculus with linear temporal logic over infinite traces. It develops a syntactic, continuation-based WP framework that supports sequential composition and iteration, while incorporating induction, coinduction, and a multi-hypothesis mechanism to handle nested temporal guarantees such as $\Box$, $\lozenge$, and $\varphi\mathcal{U}\psi$. The main contributions are (i) a set of rules for decomposing verification conditions into temporal implications, (ii) a novel $wp^*$ mechanism to accumulate inductive hypotheses and progress measures for loops, and (iii) practical demonstrations via safety and liveness examples, with formalization in Isabelle/HOL and a Scala DSL implementation. The work advances auto-active verification by providing a viable path to first-class temporal specifications, enabling automated reasoning about both safety and liveness in structured programs and paving the way fortemporal logic to become a standard feature of verification pipelines.

Abstract

Auto-active program verification rests on the ability to effectively the translation from annotated programs into verification conditions that are then discharged by automated theorem provers in the background. Characteristic such tools, e.g., Why3, Dafny, and Viper, is that this process does not involve user interaction, expecting all guiding hints like invariants to be given upfront. For sequential correctness, this paradigm is well established, thanks to approaches like weakest precondition generation and symbolic execution. However, to capture temporal properties, the specification language of choice for a broader system perspective, additional concerns and challenges are introduced into the translation and proof. Approaches based on symbolic model-checking can verify such properties on system models, e.g., using automata constructions. However, ascribing temporal properties to structured and data-intensive programs is more difficult. Several program calculi have been proposed in the literature, each of which on their own falls short in some regard of supporting an auto-active workflow. However, all essential ideas, while perhaps some are not widely acknowledged, are in fact found in the literature. In this paper, we demonstrate how to assemble these ideas into a weakest-precondition calculus for linear temporal properties and demonstrate it with examples.