Rigorous Software Development

CSCI-GA 3033-011

NYU, Graduate Division, Computer Science Course - Spring 2012


Class MeetingsMon 5:00-6:50pm in CIWW 317
First LectureJan 23, 2012
Last LectureMay 7, 2012
Final ExamMay 14, 2012, 5:00-6:50pm in CIWW 317
InstructorThomas Wies
OfficeCIWW 407
Office HoursWed 3:00-4:00pm, or by appointment.


  • 03/21/12 - The project description for the programming project is now available.
  • 02/14/12 - Important: Lecture 4 has been rescheduled to Friday, 02/24/12 5:00-6:50pm, in room WWH 312.
  • 02/13/12 - Due to the closing of Warren Weaver Hall today's class has been canceled.


Software continues to pervade our lives and is now routinely deployed in safety and security critical systems. While this technological advancement greatly benefits society it also creates a new threat: software failures with severe consequences, such as health hazards and financial repercussions. 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.


  • Design by Contract
  • Semantics of Programming Languages
  • Runtime Assertion Checking
  • Automated Test Case Generation
  • Extended Static Checking
  • Formal Verification
  • 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.

Reading Material


Exercises (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.