Rigorous Software Development

CSCI-GA 3033-009

NYU, Graduate Division, Computer Science Course - Spring 2013


Class MeetingsMon 5:00-6:50pm in CIWW 317
First LectureJan 28, 2013
Last LectureMay 13, 2013
Final ExamMay 20, 2013, 5:00-6:50pm in CIWW 317
InstructorThomas Wies
OfficeCIWW 407
Office HoursThu 3:00-4:00pm, or by appointment.


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.


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


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


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



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]


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.

Programming Project

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

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.


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.