Advances in Program Termination and Liveness

摘要

Recent research advances now allow us to automaticallyprove termination and other liveness properties of many industrial pro-grams. In cases where the desired property does not hold for all inputs,tools can be used to synthesize a precondition on the inputs under whichthe property does hold. In this tutorial I will describe these recent ad-vances and discuss our efforts to apply termination analysis to industrialsoftware.