Automated Methods for Proving Program Termination and Liveness

Proving program termination is an important step towards ensuring software reliability. The programmers expect that the majority of code fragments, including procedures, event handles, or other program components, always terminates. Unfortunately, until recently there were no viable approaches for automatically proving termination of programs written in imperative programming languages.