Integrating CCG Analysis into ACL2

---

Matt Kaufmann, Panagiotis Manolios, J S. Moore, and Daron Vroon.
The Eight International Workshop on Termination, 2006.

Introduction

ACL2 is a powerful, industrial strength theorem proving system, which has been used on numerous verification projects. It is part of the Boyer-Moore family of provers, for which its authors received the 2005 ACM Software System Award. Termination plays a central role in ACL2's logic. It is used to demonstrate the logical consistency of function definitions and allows for the admission of an induction scheme that mirrors each function's recursive structure.

In previous work we introduced calling context graphs (CCGs) and showed how they can be combined with theorem proving queries to provide a powerful method for proving termination of programs written in first order, functional programming languages. In this paper we describe work we are doing to integrate CCG-based termination analysis into ACL2.

We begin in the next section by providing relevant background on ACL2 and its current approach to termination analysis as well as the CCG approach to termination analysis. Section 3 then describes our work on extending ACL2 to include the CCG approach, with a focus on issues encountered. We conclude in Section 4.

PDF (125K)