Date: Mon, 07 Feb 2005 12:36:55 -0600
From: Jared Davis
Subject: This week in ACL2


Hi,

At this week's ACL2 meeting, I'll be talking about using ACL2 as an environment 
for formal software development.  For software systems that need to be reliable 
(compilers, database systems, whatever), the following seems like an attractive 
design methodology:

   1. Formalize the specifications for the software's behavior
   2. Validate that these specifications are really the intent
   3. Create an efficient implementation
   4. Verify that the implementation satisfies its specification

In the talk, I will talk about using this methodology in the development of an 
XML processor in ACL2.  Along the way, I'll digress about using exhaustive 
testing as a proof technique.  This technique has been quite useful to me in 
this work, and may be more widely applicable.  I'll also talk briefly about 
reasoning about state in order to be able to use the file input functions 
(read-byte$ and read-char$) from within ACL2 code that needs to be reasoned 
about and have its guards verified.

Hope to see you there,

     Jared