There is a signup schedule for this event (UT EID required).

Type
of Talk: Colloquium

Speaker/Affiliation: Byron Cook
Microsoft

Research Cambridge University

Date/Time: Wednesday October 15 20

08 11:00 a.m.

Location: ACES 2.402

Host: J Strother Moore<

br>
Talk Title: Proving That Software Eventually Does Something Good

Talk Abstract:
Recent research advances now allow us to automatical

ly prove
termination and other liveness properties of many industrial
programs. In cases where the desired property does not hold
for all in

puts tools can be used to synthesize a precondition
on the inputs under
which the property does hold. In this talk
I will describe these recent
advances and discuss our efforts
to apply termination analysis to the p

roblem of proving that
device drivers do not hang the Windows operating

system.

Speaker Bio:
Dr. Byron Cook is researcher at Microsoft''s
laboratory at
Cambridge University. His research interests include topi

cs
in program verification theorem proving and programming
languag

es. In recent years Byron has been working on
program termination shap

e analysis and software model
checking. Byron is one of the developers
behind the Windows
products called Static Driver Verifier which attem

pts to
automatically prove the correctness of Windows OS device
dri

vers with respect to a fixed set of properties. For more
information se

e
http://research.microsoft.com/%7Ebycook