We present an abstract interpretation framework for proving liveness properties of imperative programs, to ensure that some event happens once or infinitely many times during program execution. A further abstraction based on piecewise-defined ranking functions yields a static analysis that automatically infers sufficient conditions for these liveness properties as well as upper bounds on the waiting time before the event of interest occurs.
Informal abstract: How I thought I knew everything about fixpoints and widenings, until I did not.
