|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|
|Office Hours||Tue 5:00-6: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. 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.
- Design by Contract
- Formal Verification
- Program Semantics and Hoare Logic
- Foundations of SAT and SMT solvers
- Automated Testing
- Static Analysis
- Abstract Interpretation
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.
- 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
- Project homepage
- Browser version of Dafny Verifier
- Tutorial (online version)
- Dafny quick reference
- Installation Instructions
You can find the syllabus and class notes on the course's NYU classes page.
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 projects (30%), final exam (40%).
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.