X-IronPort-MID: 1799786603
X-SBRS: 4.1
X-BrightmailFiltered: true
X-Brightmail-Tracker: AAAAAQAAA+k=
X-IronPort-AV: i="4.02,153,1139205600"; 
   d="scan'208"; a="1799786603:sNHT16568884"
To: acl2-mtg@lists.cc.utexas.edu
Subject: This week in ACL2
Date: Tue, 28 Feb 2006 11:53:01 -0600
From: Robert Bellarmine Krug <rkrug@cs.utexas.edu>
Reply-To: acl2-mtg@lists.cc.utexas.edu
Sender: owner-acl2-mtg@lists.cc.utexas.edu
X-Listprocessor-Version: 8.2.10/020311/17:52 -- ListProc(tm) by CREN
X-SpamAssassin-Status: No, hits=-2.6 required=5.0
X-UTCS-Spam-Status: No, hits=-132 required=180

Greetings,

This week I will be talking about my work in support of the
Destiny tool being developed at the NSA.   I assume no background
other than familiarity with ACL2.

I will say a few, brief, words about Destiny and what it does
from the perspective of ACL2.  I will give examples of its
input and output, but will say almost nothing about how it operates.

I will then point out a couple of difficulties the ACL2 analyst
would encounter when using this output.  These are primarily
related to induction.  My current solutions to these problems
will be presented.  These solutions fall into four categories:
1. Invariant theorems
2. Call Stack-related theorems
3. Cone of Influence theorems
4. Other theorems.
I will provide examples of each, and briefly describe how I
guess the appropriate theorems.  I will also talk about what
I like or don't like about these solutions.

Robert