ISR Distinguished Speaker

David Notkin

Department of Computer Science & Engineering
“Symbolic Model Checking for Large Software Specifications: Case Studies, Optimization, and Extension”
Wednesday, April 4, 2001 - 2:00pm to 3:30pm
Faculty Host: 

Email RSVP required to Rick Martin at by Friday, March 30.

McDonnell Douglas Auditorium (building #311)

No cost to attend.


Click here for directions and parking information.


Despite its tremendous success in locating bugs in hardware circuits, symbolic model checking has rarely been applied to software. The prevalent view is that the symbolic representations used in model checking, such as binary decision diagrams (BDDs), cannot capture the complexity inherent in most software systems. Contrary to this belief, we will present some results and experience in applying the technique to the statecharts specifications of two industrial software systems: a collision-avoidance system used on most commercial aircraft and an electrical power distribution system on Boeing 777. Using symbolic model checking, we have discovered subtle but important errors not found in prior verification efforts. Although the final results are encouraging, initially many of the analyses were infeasible because of the huge BDDs generated. We have developed intuition about some factors that can cause BDD blowup, and based on the insights, devised optimization techniques to improve the efficiency of the analyses by orders of magnitude. These optimizations have made feasible certain analyses that were previously intractable. This is primarily the work of William Chan, with involvement from Richard Anderson, Paul Beame, David Notkin, David Jones, and Bill Warner.

About the Speaker: 

David Notkin received his Bachelor's in computer science, cum laude with honors, from Brown University in 1977, and his Ph.D. in computer science from Carnegie Mellon University in 1984. He joined the faculty of the Department of Computer Science & Engineering at the University of Washington in 1984 and now is the Boeing Professor and Associate Chair. His honors and awards include a 1988 National Science Foundation Presidential Young Investigator Award, an ACM Fellow, the 2000 University of Washington Distinguished Graduate Mentor Award. He has served on the editorial boards of the ACM Transactions on Software Engineering and Methodology and the IEEE Transactions on Software Engineering for several years. He served program chair for the 1st ACM SIGSOFT Symposium on the Foundations of Software Engineering and as program co-chair for 17th International Conference on Software Engineering. He finishing his fourth year as the chair of ACM SIGSOFT. He has advised 13 Ph.D. students and several dozen Masters students; two of them (Ernst and Chan) won Honorable Mentions in the most recent ACM Doctoral Dissertation Award competition.