Information

Class Meetings	Mon 5:00-6:50pm in CIWW 317
First Lecture	Jan 28, 2013
Last Lecture	May 13, 2013
Final Exam	May 20, 2013, 5:00-6:50pm in CIWW 317
Instructor	Thomas Wies
Office	CIWW 407
Office Hours	Thu 3:00-4:00pm, or by appointment.

Overview

Software is increasingly pervading our lives and is now routinely deployed in safety and security critical systems. While this technological progress benefits society greatly, it also creates a new threat: software errors with severe consequences including health hazards, financial repercussions, and security vulnerabilities. Today, reports about security threads caused by software errors hit the news almost daily. How can one ensure that software works reliably? Program Verification is the area of computer science that studies mathematical methods to answer this question. In the last decade, Program Verification has brought forth sophisticated tools that assist software engineers in building reliable software. In this course, we will explore these tools. We will learn how they are used to enable rigorous software development, and we will study the algorithms that work under their hoods. The course will be accompanied by programming projects making use of these tools.

Topics

• Modeling Software
• Design by Contract
• Runtime Assertion Checking
• Automated Test Case Generation
• Formal Verification
• Semantics of Programming Languages
• Static Analysis

Tools

The list of tools that we will discuss in the course includes:

• Alloy
• JML
• JMLUnit
• Korat
• Dafny

Prerequisites

This course will be open to MS and PhD students. Participants should have basic understanding of mathematical concepts such as sets and relations and the ability to write mathematical proofs. Also, basic programming experience in Java is assumed. Preliminary knowledge in Logics and Verification is useful but not mandatory. The course is self-contained and any required background knowledge is taught in class.

Course Material

Recommended Reading

• Software Abstractions: Logic, Language, and Analysis (revised edition) by Daniel Jackson, The MIT Press, 2012
• Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edition by Michael Huth and Mark Ryan, Cambridge University Press, 2004
• The Formal Semantics of Programming Languages by Glynn Winskell, The MIT Press, 1993
• Design by Contract with JML by Gary T. Leavens and Yoonsik Cheon
• JML Reference Manual (Draft) by Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman, July 2011.

Dafny

• Project homepage
• Browser version of Dafny Verifier
• Tutorial (online version)
• Dafny quick reference
• Installation Instructions

Schedule

Week	Date	Topics	Materials
1	01/28	Introduction	Slides [pdf]; Dafny code; Alloy code; Suggested reading: ch. 1, 2.1-2.3 of SA
2	02/04	Alloy Language	Slides [pdf]; Code: hierarchical address book; Suggested reading: ch. 3 and 4 of SA
3	02/11	Alloy Language; Modeling Techniques: Traces, Invariants, Abstraction, Refinement, and Conformance	Slides [pdf]; Code: address book with traces, event-based address book, memory models Suggested reading: ch. 2-4 and 6 of SA
4	02/18	no class (Presidents day)
5	02/25	Alloy Analyzer; Introduction to Propositional Logic	Slides [pdf]; Suggested reading: ch. 5 of SA; ch. 1 of Logic in Computer Science
6	03/04	Design by Contract; Introduction to JML	Slides [pdf];
7	03/11	Introduction to JML: Method Contracts, Class Invariants, Model and Ghost Fields, Data Groups; Runtime Assertion Checking	Slides [pdf]; Code: PriorityQueue.java, Heap.java, Test.java
8	03/18	no class (spring break)
9	03/25	Automated Test Case Generation: JMLUnit, Korat	Slides [pdf]
10	04/01	Program Verification with Dafny	Slides [pdf]; Dafny examples
11	04/08	Class Invariants and Framing: Ownership Types, Dynamic Frames	Slides [pdf]; Dafny example
12	04/15	Semantics of Programming Languages; Operational Semantics of Java and JML	Slides [pdf]; Suggested reading: ch. 2 of Winskell's book
13	04/22	Axiomatic Semantics; Hoare Logic	Slides [pdf]; Suggested reading: ch. 6 and 7 of Winskell's book
14	04/29	Hoare Logic; Verification Condition Generation	Slides [pdf]; Suggested reading: ch. 6 and 7 of Winskell's book
15	05/06	Static Program Analysis; Predicate Abstraction	Slides [pdf]
16	05/13	Counterexample-Guided Abstraction Refinement; Automated Debugging	Slides [pdf]

Homework

For submission of solutions, please follow the instructions on the assignment sheets. Sample solutions to homework assignments will be available after the submission deadline has passed.

• Homework 1 (due 02/11)
• Homework 2 (due 02/18)
• Homework 3 (due 02/25)
• Homework 4 (due 03/11)
• Homework 5 (due 03/11)
• Homework 6 (due 03/25), additional material
• Homework 7 (due 04/01), additional material
• Homework 8 (due 04/08), additional material
• Homework 9 (due 04/15), additional material
• Homework 10 (due 04/22)
• Homework 11 (due 05/06)

Programming Project

You can choose one of the following two projects. The projects are due on May 22 May 18.

• Project 1: Perfect Minesweeper Solver (additional material)
• Project 2: Dijkstra's Algorithm (additional material)

Mailing List

All course-related announcements will be sent to the course mailing list. You may also use this list to ask questions and discuss issues related to the course. If you have enrolled before the start of the term, you are automatically subscribed to the list. Otherwise, use the above link to subscribe manually.

Grading

Homework (30%), term project (30%), final exam (40%).

Academic Integrity

Please review the departmental academic integrity policy. In this course, you may discuss homework problems and assignments with other students, but the work you turn in must be your own. Do not copy another student's work. Also, you should consult the instructor before using materials or code other than that provided in class. Copying code or other work without giving appropriate acknowledgment is a serious offense with consequences ranging from no credit to potential expulsion.