Authorship Disclaimer. The lecture slides on this page are intended to serve as teaching instruments for a course on Software Engineering. While the slides were formatted by Dr. Sridhar, the content is compiled from other sources, including the readings listed on the course website, other books on Software Engineering and various internet materials. In almost every case, the ideas belong to someone other than Dr. Sridhar. Indeed, text is often quoted verbatim without an explicit citation (to improve the readability of the slides). The original authors retain all copyrights. If you are interested in citing any of the material in these slides, please contact Dr. Sridhar for the original source(s). DO NOT CITE THESE PRESENTATIONS. THE CONTENT SHOULD NOT BE ATTRIBUTED TO DR. SRIDHAR. SEE DR. SRIDHAR IF YOU HAVE ANY QUESTIONS.
The following is a fairly accurate schedule of how we will proceed through our lectures. We may change the schedule a bit depending of how the class progresses through the material.
HR below refers to the course textbook (Huth & Ryan).
| Date | Topic | Reading | Homework |
| Wed 1/21/09 |
Introduction; The basics (Sets, relations, functions, booleans)
Lecture notes |
||
| Mon 1/26/09 | Class canceled due to bad weather | ||
| Wed 1/28/09 | Propositional logic; Natural deduction | HR 1.1, 1.2 | |
| Mon 2/02/09 | Propositional logic; Natural deduction | HR 1.2, 1.3 | |
| Wed 2/04/09 | Semantics of Propositional logic | HR 1.4 | Homework 1 Handout |
| Mon 2/09/09 | Semantics of Propositional logic | HR 1.4 | Homework 1 Handin |
| Wed 2/11/09 | Predicate logic; Proof theory | HR 2.1, 2.2 | Homework 2 Handout |
| Mon 2/16/09 | President's Day - University holiday | ||
| Wed 2/18/09 | Predicate logic; Proof theory | HR 2.2, 2.3 | Homework 2 Handin |
| Mon 2/23/09 | Semantics of Predicate logic | HR 2.4 | Homework 3 Handout |
| Wed 2/25/09 | Specifying concurrent systems; UNITY notation | ||
| Mon 3/02/09 | Safety and Liveness properties of concurrent systems | Homework 3 Handin | |
| Wed 3/04/09 | Proving properties of concurrent systems | ||
| Mon 3/09/09 | SAC 09 - no class | ||
| Wed 3/11/09 | Mid-term Exam (in class) | ||
| Mon 3/16/09 | Spring break | ||
| Wed 3/18/09 | Spring break | ||
| Mon 3/23/09 | Introduction to model checking; Temporal logics; LTL | HR 3.1, 3.2 | Project abstracts due |
| Wed 3/25/09 | LTL Model checking | HR 3.2, 3.6.3 | |
| Mon 3/30/09 | Model checking system properties | HR 3.3 | Homework 4 Handout |
| Wed 4/01/09 | CTL Model checking | HR 3.4, 3.6.1 | |
| Mon 4/06/09 | Model checking algorithms | HR 3.6.3 | Homework 4 Handin |
| Wed 4/08/09 | Binary decision diagrams | HR 6.1 | |
| Thu 4/09/09 | Reduced OBDDs | HR 6.2 | Homework 5 Handout |
| Mon 4/13/09 | IPSN '09 -- no class | ||
| Wed 4/15/09 | IPSN '09 -- no class | ||
| Mon 4/20/09 | Program verification; Partial and total correctness; Hoare logic | HR 4.1, 4.2 | Homework 5 Handin |
| Wed 4/22/09 | Proving partial correctness | HR 4.3 | Homework 6 Handout |
| Mon 4/27/09 | Proving total correctness | HR 4.4 | |
| Wed 4/29/09 | Program verification tools | Homework 6 Handin; Homework 7 Handout | |
| Mon 5/04/09 | Class presentations | ||
| Mon 5/06/09 | Class presentations | Homework 7 Handin | |
| Mon 5/11/09 | Final Exam |