Proving Conditional Termination

Abstract

We describe a method for synthesizing reasonable underapproximations to weakest preconditions for termination---a long-standing open problem. The paper provides experimental evidence to demonstrate the usefulness of the new procedure.