Erik Reeber, 9/28/05, ACL2 seminar

X-IronPort-MID: 1625265906
X-SBRS: 4.2
X-BrightmailFiltered: true
X-Brightmail-Tracker: AAAAAA==
X-Ironport-AV: i="3.97,150,1125896400"; 
   d="scan'208"; a="1625265906:sNHT13879312"
Date: Tue, 27 Sep 2005 16:08:04 -0500 (CDT)
From: "Erik H. Reeber" 
To: acl2-mtg@lists.cc.utexas.edu
Subject: This weeks ACL2 Seminar
In-Reply-To: <200508151342.j7FDg0WJ017117@craigievar.cs.utexas.edu>
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
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=-232 required=180


Hello everyone,

    In this week's ACL2 meeting, after the usual round-table discussion,
I'll be giving a practice talk for my presentation at CHARME next week.
I'll be presenting the paper Warren and I wrote on the DE2 language.
The presentation should only be 25 minutes, but you all should slow me
down by asking questions and giving feedback.

    The paper is available on my web site at:

Here's the abstract:

We formalized the DE2 hierarchical, occurrence-oriented finite
state machine (FSM) language, and have developed a proof
theory allowing the mechanical verification of FSM
descriptions.  Using the ACL2 functional logic, we have
defined a predicate for detecting the well-formedness of DE2
expressions.  Furthermore, we have defined a symbolic
simulator for DE2 expressions which also serves as a formal
cycle-based semantics for the DE2 language.  DE2 is deeply
embedded within ACL2, and the DE2 language includes an
annotation facility that can be used by programs that
manipulate DE2 descriptions.  The DE2 user may also specify
and prove the correctness of programs that generate DE2
descriptions.  We have used DE2 to mechanically verify
components of the TRIPS microprocessor implementation.