CISC422/853: Formal Methods in Software Engineering: Computer-aided Verification (Winter 2009) Readings (Lecture slides, tool descriptions, papers) [Home] [Content] [Schedule] [Readings] [Assignments] [Tools] [Projects] [Messages]

Lecture slides

1. Intro (first used: Mon, Jan 05) [pdf (4up)]
2. A few words about concurrency (first used: Thurs, Jan 08) [pdf (4up)]
3. Modeling (first used: Mon, Jan 12; last updated: Thurs, Jan 15) [pdf (4up)]
4. Intro to BIR and Bogor (first used: Tue, Jan 20) [pdf (4up)]
5. Model checking I (first used: Mon, Jan 26) [pdf (4up)]
6. Intro to Promela and Spin (first used: Thurs, Jan 29) [pdf (4up)]
7. Specifying (first used: Thurs, Feb 5; last updated: Wed, Mar 4) [pdf (4up)]
8. Model checking II (first used: Thurs, Feb 26; last updated: Wed, Mar 4) [pdf (4up)]
9. Optimization (first used: Thurs, Mar 5; last updated: Thurs, April 2) [pdf (4up)]
10. Overview over software model checking tools (first used: Tue, Mar 24; last updated: Thurs, April 2) [pdf (4up)]

Tutorial slides

1. Tutorial 1 (Jan 28, put together by Scott Grant) [pdf]
2. Tutorial 2 (Feb 11, put together by Scott Grant) [pdf]
3. Tutorial 3 (March 25, put together by Scott Grant) [pdf]

Notes

1. Course notes on CTL and CTL model checking [pdf]
2. Notes on control flow analysis and slicing [pdf]

Code

1. The Java code for the Ornamental Garden problem is here. More demo concurrent programs in Java can be found on the website for the book "Concurrency: State Models & Java Programs" by J. Kramer and J. Magee.
2. The shared variable C code is demo1.c and demo2.c.

General

• Safety Critical Systems: Challenges and Directions. J.C. Knight. ICSE '02. Orlando, Florida. May. 2002. [pdf]
• Formal Methods: State of the Art and Future Directions. E. Clarke and J. Wing. Report by the Working Group on Formal Methods for the ACM Workshop on Strategic Directions in Computing Research, ACM Computing Surveys, vol. 28, no. 4, December 1996, pp. 626-643. [ps, pdf]
• The Risks Digest. A moderated forum on risks to the public in computers and related systems.
• Article on the skill of being able/willing to pay attention to detail in the IT industry:
  • A closer look at attention to detail. Communications of the ACM. Vol 48, No 7. July 2005. [pdf].
• Article on the increased use of concurrency in software:
  • The Free Lunch Is Over: A Fundamental Turn Toward Concurrency in Software. Herb Sutter. Dr. Dobb's Journal. Vol 30. No 3. March 2005. [pdf].
• Article on the importance of good design
  • Battling Google, Microsoft Changes How It Builds Software. Robert A. Guth. Wall Street Journal Online. September 23, 2005. [pdf].
• Various popular science articles on the sloppiness in the IT industry:
  • Why Software Fails. Robert N. Charette. IEEE Spectrum. September 2005. [pdf]
  • A closer look at attention to detail. James J. Cappel, Victor R. Prybutok, and Benny Varghese. Communications of the ACM, July 2005, Vol 48, No. 7. [pdf]
  • Building Better Software with Better Tools. Steven J. Vaughan-Nichols. IEEE Computer, September 2003.
  • Why Software Is So Bad, Technology Review, June 17, 2002. [ps, pdf]
  • Will Bugs Eat Up The US Lead In Software?, Business Week, December 1999. [ps, pdf]
  • High Tech's Missionaries of Sloppiness?, Salon.com, December 2000. [ps, pdf]
  • Comments on Software Quality, Watts S. Humphrey, CMU SEI. [ps, pdf]

Last modified: Thu Apr 2 13:14:45 EDT 2009