There is a sign-up schedule for this event that can be found at

http://www.cs.utexas.edu/department/webevent/utcs/events/cgi/list_event

s.cgi

Type of Talk: UTCS Colloquia

Speaker/Affiliation: Professor
Fei Xie/Computer Science, Portland State University

Talk Audience: U

TCS Faculty, Grad Students, and Outside Interested Parties

Date/Time

: April 26, 2011, 1:00 p.m.

Location: ACES 2.402

Host: Jim Brow

ne

Talk Title: Automata-Theoretic Approach to Hardware/Software Co-ver

ification

Talk Abstract: In this talk, we present an automata-theoret

ic approach to hardware/software (HW/SW) co-verification. We have designed

a co-specification framework to formally specify HW/SW interface protocols

; we have synthesized a hybrid Buchi Automaton Pushdown System, namely Buc

hi Pushdown System (BPDS), as the unifying formal model for HW/SW interfac

es; and we have developed a co-verification tool, CoVer, that not only i

mplements our model checking algorithms but also realizes our reduction alg

orithms for BPDS. Application of our approach to the Windows device/driver

framework has resulted in the detection of fifteen specification issues. Fu

rthermore, utilizing CoVer, we have discovered twelve real bugs in five p

roduction drivers.

Speaker Bio: Fei Xie is an associate professor in t

he Department of Computer Science, Portland State University. His interest

s are primarily in the areas of software engineering, embedded systems, a

nd formal methods, particularly development of formal method based techniq

ues and tools for building safe, secure, and reliable software and embedd

ed systems.