[BB] Boehm and Basili, “Software Defect Reduction Top 10 List,” Computer, January 2001.
[BAN] M. Burrows, M. Abadi, and R. Needham, “A Logic of Authentication,” ACM Transactions on Computer Systems, vol. 8, no. 1, February 1990, pp. 18—36. Earlier version available as DEC/SRC technical report 39, 1989.
[Bloom] Bard Bloom, “Seeing by Owl-Light: Symbolic Model Checking of Business Application Requirements,” submitted to POPL’02. Draft July 2001. Please do not circulate copies without permission.
[CGP] Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled, Model Checking, The MIT Press, 1999.
[E99] Robert J. Ellison, David A. Fisher, Richard C. Linger, Howard F. Lipson, Thomas A. Longstaff, and Nancy R. Mead, Survivability: Protecting Your Critical Systems, IEEE Internet Computing, November-December 1999, pp. 55-63.
[Gries] Gries, David, The Science of Programming, Springer-Verlag, 1981, Chapter 15.
[ELTM] Ellison, Linger, Longstaff, and Mead, “A Case Study in Survivable Network System Analysis,” IEEE Software, July-August 1999.
[HJ1] Hoare and Jones, Procedures and Parameters: An Axiomatic Approach, in Essays in Computing Science.
[HJ2] Hoare and Jones, Proof of Correctness of Data Representation, in Essays in Computing Science.
[Jain0] Raj Jain, The Art of Computer Systems Performance Analysis, John Wiley and Sons, 1991, pp. 507—518.
[Jain1] Raj Jain, The Art of Computer Systems Performance Analysis, John Wiley and Sons, 1991, pp. 547—569.
[Jain2] Raj Jain, The Art of Computer Systems Performance Analysis, John Wiley and Sons, 1991, pp. 519--546.
[KMM] R. Kemmerer, C. Meadows, and J. Millen, “Three Systems for Cryptographic Protocol Analysis,” Journal of Cryptology, vol. 7, no. 2, 1994, pp. 79—130.
[Ryan] Ryan, Peter Y. A. and Sven Dietrich, "Survivability, the Universe, and Everything," Extended abstract submitted to WITS-02, Workshop on Issues in the Theory of Security (WITS-02), 14-15 January 2002, Portland Oregon, USA.
[Satya] Satyanarayanan, M. , "A Survey of Distributed File Systems," Annual Review of Computer Science, 1990, Volume 4, pp. 73-104.
[SM] Sneed and Majnar, “A Case Study in Software Wrapping,” Proc. Of the International Conference on Software Maintenance, IEEE Computer Society Press, November 1998, pp. 86—93.
[Wing87] J.M. Wing, "A Larch Specification of the Library Problem," Proceedings of the Fourth International Workshop on Software Specification and Design, Monterey, CA, April 1987, pp. 34-41. Also CMU-CS-86-168, December 1986.
[Wing88] J.M. Wing, "A Study of Twelve Specifications of the Library Problem," IEEE Software, vol. 5, no. 4, July 1988, pp. 66-76. Also CMU-CS-87-142, July 1987.
[Wing96] J.M. Wing, "Hints to Specifiers," in Teaching and Learning Formal Methods, Dean and Hinchey, editors, Academic Press, 1996, Chapter 5, pp. 57-77. Also available as CMU-CS-95-118R, May 1995.
Course Schedule
Handouts
Homework
Laboratory Assignments
SMV Manual