David Notkin: Software Model Checking

Our research on model checking was intended to determine if the successes of model checking in hardware could be applied successfully to software-oriented descriptions. Overall, we showed that we could indeed apply symbolic model checking to software specifications, including significant parts of two large, industrial-strength specifications: TCAS II and a fault-tolerant power distribution model approximating that used on the Boeing 777.

William Chan was the heart and soul of this research. William died in a tragic automobile accident one week after defending his dissertation and a month before starting an assistant professorship at Brown University. A dissertation award at the University of Washington Department of Computer Science & Engineering has been endowed in his memory.

Dissertation

William Chan. Symbolic Model Checking for Large Software Specifications. Ph.D. Dissertation, Department of Computer Science & Engineering, University of Washington (2000).

Key publications

William Chan, Richard J. Anderson, Paul Beame, David. H. Jones, David Notkin and William. E. Warner. Decoupling Synchronization from Logic for Efficient Symbolic Model Checking of Statecharts. ICSE99, 21st International Conference on Software Engineering (May 1999).
William Chan, Richard J. Anderson, Paul Beame and David Notkin. Improving Efficiency of Symbolic Model Checking for State-Based System Requirements. ISSTA 98: Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 102-112, March 1998, Clearwater Beach, Florida, USA.
William Chan, Richard J. Anderson, Paul Beame, and David Notkin. Combining Constraint Solving and Symbolic Model Checking for a Class of Systems with Non-linear Constraints. Computer Aided Verification, 9th International Conference, CAV'97 Proceedings, LNCS 1254, pages 316-327. Springer-Verlag, June 1997, Haifa, Israel.
William Chan, Richard J. Anderson, Paul Beame, Steve Burns, Francesmary Modugno, David Notkin, and Jon D. Reese. Model Checking Large Software Specifications. IEEE Transactions on Software Engineering 24,7, pp. 498--520, July 1998. An earlier version appeared in SIGSOFT'96: Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundation of Software Engineering, pages 156-166, October 1996, San Francisco, USA.
- Download paper (pdf)

Talks

Lecture slides (html)