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.
Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Ryb