Proving Conditional Termination
- Byron Cook ,
- Sumit Gulwani ,
- Tal Lev-Ami ,
- Andrey Rybalchenko ,
- Mooly Sagiv
CAV '08 Proceedings of the 20th international conference on Computer Aided Verification |
Published by Springer-Verlag Berlin, Heidelberg
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.