Exploiting structural information to improve the analysis of discrete-state systems

Speaker:	Professor Gianfranco CIARDO
		Department of Computer Science and Engineering
		University of California at Riverside

Title:		"Exploiting structural information to improve the
		 analysis of discrete-state systems"

Date:		Monday, 12 October, 2009

Time:		4:00pm - 5:00pm

Venue:		Lecture Theatre F
		(Leung Yat Sing Lecture Theatre, near lifts 25/26), HKUST

Abstract:

Binary decision diagrams (BDDs) are a success story in the field of
computing: fter the seminal 1986 paper by R. Bryant, BDDs have been widely
adopted for the verification of hardware chips, communication protocols,
and distributed algorithms.  While BDDs represent an enormous improvement
with respect to traditional explicit methods where states are stored and
processed one at a time, many practical software verification problems
remain out of reach. In this talk, we show how enormous efficiency can be
further gained by employing new variants of decision diagrams and
exploiting the structure of the system, namely the fact that, while the
system state is described by many variables, most system events depend and
affect only a handful of them. The resulting algorithms are shown to be
superior to the symbolic breadth-first iterations usually employed with
BDDs, and to be applicable not just to state-space generation and CTL
model checking, but even to integer- Valued problems such as the
generation of the distance function. We illustrate how our techniques were
employed to verify the Runway   Incursion Prevention System, a software
safety component being developed by NASA


********************
Biography:

Gianfranco Ciardo is a Professor in the Department of Computer Science and
Engineering at the University of California, Riverside. Previously, he has
been on the faculty at the College of William and Mary, Williamsburg,
Virginia, a Visiting Professor at the University of Torino, Italy, and the
Technical University of Berlin, Germany, and has held research positions
at HP Labs (Palo Alto, California), ICASE (NASA Langley Research Center,
Hampton, Virginia), Software Productivity Consortium (Herndon, Virginia),
and CSELT (Torino, Italy). He received a PhD degree in Computer Science in
1989 from Duke University, Durham, North Carolina, and a Laurea in Scienze
dell' Informazione in 1982 from the University of Torino, Italy. He has
been on the editorial board of IEEE Transactions on Software Engineering
and is on the editorial board of Transactions on Petri Nets and Other
Models of Concurrency. He was keynote speaker at PNPM'01 (Achen, Germany),
ATPN'04 (Bologna, Italy), and EPEW/WS-FM'05 (Versailles, France). He is
interested in theoretical research and practical tool building for logic
and stochastic analysis of discrete-state models, symbolic model checking,
performance and reliability evaluation of complex hardware/ software
systems, Petri nets, and Markov models.