Information
| Class Meetings | Mon 5:00-6:50pm in CIWW 317 |
| First Lecture | Jan 23, 2012 |
| Last Lecture | May 7, 2012 |
| Final Exam | May 14, 2012, 5:00-6:50pm in CIWW 317 |
| Instructor | Thomas Wies |
| Office | CIWW 407 |
| Office Hours | Wed 3:00-4:00pm, or by appointment. |
News
- 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.
Overview
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.
Topics
- Design by Contract
- Semantics of Programming Languages
- Runtime Assertion Checking
- Automated Test Case Generation
- Extended Static Checking
- Formal Verification
- Static Analysis
Tools
The list of tools that we will discuss in the course includes:
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.
Reading Material
- Software Abstractions: Logic, Language, and Analysis by Daniel Jackson, The MIT Press, 2006
- Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edition by Michael Huth and Mark Ryan, Cambridge University Press, 2004
- 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.
- The Java Language Specification, third edition by James Gosling, Bill Joy, and Guy Steele
- The Java Virtual Machine Specification, second edition by Tim Lindholm and Frank Yellin
Grading
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.
