Weakest Precondition Rules for Programs with Linear Temporal Specifications

Abstract With today’s mature auto-active program verification tools complex functional requirements can be formalized and proved. To that end, they rely on verification condition generation to bridge between structured programs and high-level specifications and the automated theorem provers used in the background. Integrating software modules into larger systems may necessitate to consider temporal logic requirements, notably liveness properties over infinite traces. Unfortunately, most state-of-the-art tools lack explicit support for such temporal specifications. There are various proposals that address the integration of structured programs and temporal logic, but each comes with some inherent limitation regarding expressiveness or automation. In this paper, we demonstrate a simple but universal solution that can be integrated easily into existing verification condition generators.