UTCS Oral Proposal: Qiang Zhang/UTCS Automating the verification of machine-level programs for operational machines in ACES 3.408

Contact Name: 
Jenna Whitney
Aug 10, 2006 3:30pm - 5:30pm

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

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

verify a large class of programs for that machine. The
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.

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

broad constraints). We demonstrate it on several simpler

ional models.