Information

Class Meetings	Mon 7:10-9:00pm in CIWW 317
First Lecture	Jan 25, 2016
Last Lecture	May 9, 2016
Final Exam	May 16, 2016, 7:10-9:00pm in CIWW 317
Instructor	Thomas Wies
Office	CIWW 407
Office Hours	Tue 5:00-6: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. These tools are now routinely used in the software industry including companies such as Facebook, Google, and Microsoft.

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 and that implement some of their core algorithms.

Topics

• Design by Contract
• Formal Verification
• Program Semantics and Hoare Logic
• Foundations of SAT and SMT solvers
• Automated Testing
• Static Analysis
• Abstract Interpretation

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 simple mathematical proofs. Also, basic programming experience in Java is assumed.

Course Material

Recommended Reading

• 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

Dafny

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

Syllabus

You can find the syllabus and class notes on the course's NYU classes page.

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