Today, automated reasoning about program behavior is a well-established discipline in computer science, with a wide array of tools and techniques. In the most common scenario, the goal is to prove trace properties of programs, such as termination or functional correctness.