Non-termination bugs

Symbolic Liveness Analysis of Real-World Software

Liveness violation bugs are notoriously hard to detect, especially due to the difficulty 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 …