Principles of Software Engineering
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
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 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.
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