inherent in applying formal methods to real-world programs. We present a generic and
practically useful liveness property which defines a program as being live as long as it will
eventually either consume more input or terminate. We show that this property naturally
maps to many different kinds of real-world programs. To demonstrate the usefulness of our
liveness property, we also present an algorithm that can be efficiently implemented to …