{Automata-Based Verification of Temporal Properties on Running Programs}