Integrating Static Analysis and General-Purpose Theorem Proving for Termination Analysis

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

Last modified: Thu Jul 20 06:07:30 EDT 2006 manolios@cc.gatech.edu

Back to Pete's home page College of Computing