A Weakest Precondition Calculus for Programs and Linear Temporal Specifications

TL;DR

This paper develops a weakest precondition calculus for verifying linear temporal properties in programs, enabling automated, non-interactive proof generation for temporal correctness.

Contribution

It introduces a novel weakest precondition calculus that integrates linear temporal logic into program verification workflows.

Findings

Successfully applied to example programs demonstrating temporal property verification.

Bridges the gap between traditional program verification and temporal logic.

Supports auto-active verification with minimal user guidance.

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.