CISC 403/603: Software Verification: Fall 2009

Description:

Verification is one of the most essential tasks in any engineering endeavor. The goal of software verification is to show that a computer program meets its specification. This class focuses on formal approaches to this problem, such as temporal logic specification and model checking, symbolic execution, and static analysis. In addition to learning the theoretical foundations of these techniques, students will gain practical experience using state-of-the-art verification tools.

This year, the course will focus primarily on Model Checking.

Fundamentals:

Instructor: Stephen F. Siegel, email: mylastname@cis.udel.edu, phone: 302-831-0083
Office and Office Hours: Smith 432, TBA
Class meetings: 5:00-6:15 PM, Mon/Wed starting Sep. 2, 2009
Required Text: Principles of Model Checking, by Christel Baier and Joost-Pieter Katoen, MIT Press, 2008
Additional Recommended Texts: Model Checking, by Edmund M. Clarke, Orna Grumberg and Doron A. Peled, MIT Press, 2000
The Spin Model Checker: Primer and Reference Manual, by Gerard J. Holzmann, Addison-Wesley, 2003
Course web page: http://vsl.cis.udel.edu/603

Syllabus:

The course will follow the Baier & Katoen textbook closely. We will aim to cover most of the topics in the first 6 chapters. In addition we will study and use the Spin model checker. Readings will be assigned in advance and students are expected to complete the reading assignments by the specified dates so that they will be in a better position to understand the lectures and participate in class discussions.

The topics are as follows (the number in parentheses is the approximate number of course days allocated for that topic):

Introduction and System Verification (1)

the nature of software defects, overview of verification approaches, model checking

Modeling Concurrent Systems (5)

transition systems, modelling concurrent systems with NanoPromela, Spin

Linear-Time Properties (5)

deadlock, linear-time behavior, safe properties and invariants, liveness, fairness

Regular Properties (5)

automata on finite and infinite words, model checking omega-regular properties, nested depth-first search

Linear Temporal Logic (5)

syntax of LTL, semantics of LTL, automata-based LTL model checking

Computation Tree Logic (7)

syntax and semantics of CTL* and CTL, expressiveness of CTL vs. LTL, CTL model checking, symbolic CTL model checking using binary decision diagrams

Assessment:

There will be 5 or 6 problem sets (60% of grade), an in-class midterm (15%), and a final exam during finals week (20%). Class participation will also be taken into consideration (5%). Students registered for 603 (honors undergraduate students and graduate students) will have a few additional problems to complete on the problem sets.

Academic honesty:

You are encouraged to work with your classmates on the problem sets, but what you submit must be your own work. While I realize this does not define the border between right and wrong perfectly, there are some actions that clearly fall on the wrong side, such as simply copying someone else's solution to a problem or copying a solution found on the Internet. Contact me at any time if you have questions about this policy. You may use resources such as books, articles, and Internet sources, as long as you cite every resource used in your solutions. You cannot discuss the problem sets with anyone outside the class without getting permission from me first. The exams are closed book and cheating in any way will not be tolerated and will result in disciplinary action.

Attendance and Punctuality:

I understand that everyone has to miss a class or arrive late now and then. However, repeat offenders will be assigned additional homework and have the problem set component of their grade adjusted accordingly. Attendance and punctuality will also be factors in the class participation component of the grade.