Speaker Name/Affiliation: Qiang Zhang/UTCS

Date/Time: August 10 2006 at 3:30 p.m.

Location: ACES 3.408
<

br>Host: J Moore

Talk Title: Automating the verification of machin

e-level programs for operational machines

Talk Abstract:
We propo

se an approach to automating the verification of
machine-level programs
for an arbitrary abstract computing
machine provided that the semantic

s is given formally by
an operational semantics (satisfying certain bro

ad constraints).
Using the tool described here a user with a formal o

perational
semantics model of a computing machine (in ACL2) can automat

ically
verify a large class of programs for that machine. The
tool
is independent of the particular operational semantics.
That is give

n a machine defined operationally e.g. the
JVM a piece of machine-le

vel program e.g. a Java byte-code
program and a specification of thi

s piece of program we
show how to automatically generate an ACL2 book
which states
the correctness of the program and includes lemmas that <

br>will lead ACL2 automatically to the proof of the correctness.
If

the book cannot be processed automatically the user
may still edit it

to insert additional lemmas as needed.
We automate all but the %60%60c

reative'''' part of the proof.
While we demonstrate our technique for

a JVM model the
technique applies generally to any model (within certa

in
broad constraints). We demonstrate it on several simpler
operat

ional models.