Weakest Precondition Rules for Programs with Linear Temporal Specifications

Gidon Ernst

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…