Formal Verification of Temporal Programs