Date: Tue, 18 Apr 2006 10:42:27 -0500
From: Sol Swords
Subject: ACL2 seminar, April 19


Hi all,

We'll have the ACL2 meeting Wednesday in Aces 3.116 at 4:00 as usual.  
Qiang will be giving the talk.  He writes:

>I will give a talk about my work on automating the verification of
>machine-level program for an abstract computing machine provided that the
>semantics is given formally by an operational semantics. That is, given a
>machine defined operationally, i.e. JVM, a piece of machine-level program,
>i.e. a Java byte-code program, and a specification of this piece of program, we
>try to automatically generate an ACL2 book, which states the correctness of the
>program and includes that will lead ACL2, automatically, to the proof of the
>correctness.
>
Hope to see you all there,
 - Sol