Integrating Static Analysis and General-Purpose Theorem Proving for Termination Analysis
Panagiotis Manolios and Daron Vroon.
ICSE'06, The 28th International Conference on Software Engineering, Emerging Results, 2006. © ACM
We present emerging results from our work on termination
analysis of software systems. We have designed a static analysis
algorithm which attains increased precision and flexibility by
issuing queries to a theorem prover. We have implemented our
algorithm and initial results show that we obtain a significant
improvement over the current state-of-the-art in termination
analyses. We also outline how our approach, by integrating
theorem proving queries into static analyses, can significantly
impact the design of general-purpose static analyses.
PDF (91K) © ACM