Principles of Software Engineering
Project 0 (due Jan. 12, 2012)
1. Install and try Code Contracts. See slide 28 of syllabus
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
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 DafnyLibrary.zip
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
Slides and notes from class 5 (Feb. 9, 2012)
Introduction to modeling with FORMULA: Part 1
and Part 3
Examples from class available here
. FORMULA can be downloaded 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