CISC/CMPE422, CISC835: Formal Methods in Software Engineering (Fall 2019)
Readings (Lecture notes, slides, tool descriptions, examples, papers)
"Required" marks readings that are required for the course.
- Course Overview.
J. Dingel. Powerpoint slides of lectures during Week 1, Fall 2019.
- Chris Newcombe, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff.
How Amazon Web Services Uses Formal Methods.
Communications of the ACM 58(4):66-73. April 2015.
- Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, John Fitzgerald.
Formal methods: Practice and experience. ACM Computing Surveys 41(4). Oct 2009.
- Various popular science articles, including:
- The Coming Software Apocalypse. The Atlantic. Sept 26, 2017.
- Why Software Fails. R.N. Charette. IEEE Software Spectrum. Sept 2005.
Introduction and logic review
- Required (in courseware): Introduction to Temporal
Logic Model Checking. J. Dingel. Lecture notes for CISC422.
Pages 131 - 193.
- Required (on web): NuSMV 2.6 User manual. A. Cimatti and M. Roveri.
- Some instructions on using NuSMV at Queen's are here.
- Sample SMV programs used in class:
Note that some of the above documents contain several programs. To run
these programs, each program has to be put into a separate file.
- Slides on CTL and CTL model checking algorithm are here (used Nov 25, 27, and 28)