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

Abstract

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