Principles of Software Engineering
Quarter: Winter 2012
Instructor: Ethan Jackson
Time/Place: Th 6:30 - 9:20 pm in EEB 037
Office hours: By appointment
Mailing list:
Slides and notes from class 1 (Jan. 5, 2012)

Course outline and syllabus
Code contracts (guest lecturer Francesco Logozzo*)

* Additional reading on abstract interpretation and code contracts available here.
Project 0 (due Jan. 12, 2012)

1. Install and try Code Contracts. See slide 28 of syllabus for details.
2. There is nothing to submit for this project. Get some familiarity with Visual Studio, C#, and Code Contracts.
Slides and notes from class 2 (Jan. 12, 2012)

Verification with Dafny (guest lecturer Rustan Leino*)

* Additional information about program verification available here.
Project 1 (due Jan. 29 Feb. 5, 2012 by 11:59 pm)

1. Read the instructions for the project.

2. Download the simulator and project templates from here.

3. Try to solve the problem using C# and Code Contracts. We will talk more about applying Dafny in class on Jan. 19.

4. Try to have a partial solution ready for discussion on Jan. 19.

5. DAFNY: Unzip the file and read DafyNotes.pdf to get started. Look at some examples on Rise4Fun.
Slides and notes from classes 3/4 (Jan. 26 / Feb. 2, 2012)

Introduction to model checking Part 1 and Part 2.

Tool demonstration with NuSMV.
Project 2 (due Feb. 19, 2012)

1. Download and install NuSMV.
2. Model and model check a probe docking controller. See these slides for details.
Slides and notes from class 5 (Feb. 9, 2012)

Introduction to modeling with FORMULA: Part 1, Part 2 and Part 3.

Examples from class available here. FORMULA can be downloaded from here.
Slides and notes from class 6 (Feb. 16, 2012)

Introduction to (timed) models of computation with Ptolemy II.

Introduction to hybrid system simulation with Ptolemy II.

Ptolemy II can be download from here.
Slides and notes from class 7 (Feb. 23, 2012)

Introduction to propositional / first-order logic and SAT.

Introduction to SMT solving.

Z3 can be download from here.
Project 3 (due Mar. 9, 2012)

1. See these slides for grading and project description.
2. Download and install FORMULA.

Lasted updated: Feb. 26, 2012