Teaching : CS 6962 – Software Verification | Fall 2012
Instructor: Zvonimir Rakamaric
Time: Mondays, Wednesdays 10:45am-12:05pm
Location: MEB 3147
Office hours: Catch me after class; find me in my office; email me.
Mailing list: email@example.com (everyone enrolled must subscribe)
This is a tentative course syllabus and subject to potential tweaks and updates.
Course Description and Objective
The main goal of the course is to teach students how to prove programs correct. We will study theoretical foundations underlying this task, as well as do a number of hands on exercise and homework assignments that will largely be based around actually proving example programs correct. In the second part of the course, we will cover some more advanced topics, such as proving correctness of concurrent programs. We will also explore advanced techniques behind popular software verification tools used in practice. Students completing the course will gain a solid understanding of practical software verification techniques and the underlying theory. Furthermore, students will leave with significant hands-on software verification experience.
The course won’t be based around any specific programming language or embedded system.
I intend to make the course fairly self-contained, but familiarity with mathematical logic and decision procedures will be helpful. You should also be familiar with a programming language of your choice since homework assignments will involve coding.
Grading and Policies
The final grade will be based on 40% homework assignments and 60% course project. There will be 4-5 practical homework assignments covering SAT/SMT solvers and proving correctness of programs. Each student in the class will also be responsible for completing a course project of their choice.
Academic misconduct: Please read the School of Computing Policy Statement of Academic Misconduct.
Late policy: Late homework assignments and project deliverables will not be accepted unless you contact me before the deadline and have a good reason.
Collaboration and cheating: I encourage discussing homework assignments and projects with others since that’s often a good way to learn the material. However, all students must independently write their own code and write-ups. Discussing solutions at high-level is fine. Basing your code/write-up on any other code/write-up is cheating. So, do not copy solutions from another student, do not copy solutions from the internet, do not even look at solutions from another student, do not ask for solutions on online forums (e.g., Stack Overflow). Make sure you acknowledge appropriately any outside materials you used or rely on. This includes papers, books, websites, personal communication, source code, etc.
Students with disabilities: Reasonable accommodation will gladly be provided to students with disabilities. Please let me know the situation as soon as possible. If you wish to qualify for exemptions under the Americans with Disabilities Act (ADA), you should also notify the Center for Disability Services.
The Calculus of Computation: Decision Procedures with Applications to Verification by Aaron R. Bradley and Zohar Manna. We will be somewhat following this book in the first half of the course. You should have free access at the department to an electronic version through SpringerLink.
Your project can take one of these three forms:
1) Mini research project: This is your “traditional” course project. Come up with a topic at least somewhat related to software verification. Ideally it should also overlap with your research area. Study related work. Explore new directions and invent and implement new approaches. Implement existing algorithms and evaluate them. Write a project report in the end (at most 5 pages).
2) Practical verification project: Pick either a decent size piece of real-life code, or several smaller ones, or a complex algorithm, and verify a few relevant, complex properties using your tool of choice (e.g., VCC, frama-C, Boogie, Why3). Write a report about the experience (at most 5 pages).
3) Literary review: Pick a specific software verification topic that you are interested in, and thoroughly read, analyze, evaluate, and summarize research materials related to the topic. Install and try out related tools if possible. Write a critical summary of your findings (at most 10 pages).
If you have an idea for a project that doesn’t fit into any of the listed categories, come and talk to me and I’ll try to accommodate it. If you don’t have an idea for a project, stop by my office and we’ll brainstorm a nice project for you.
Team work: I will allow at most 2 students working as a team on mini research and practical verification projects. Of course, the project size should scale accordingly. Furthermore, it should be quite clear who did what and how you split up the work on the project.
Project deliverables, presentations, grading, and deadlines:
1) Project proposal (5 points, deadline: Sep 26 at 11:59pm local time): Write at most 1 page per team describing your project plan. The proposal should include: project title, list of team members, short description of related work, and proposed work with basic milestones. It doesn’t have to be too detailed. Absolutely make sure you discuss your project idea with me at least a week before the proposal due date.
2) Related work presentation (20 points, Oct 15, 17, 29, 31 in class): Present in class a paper related to your project. Every student has to present (at least) one paper. Presentation length: 15 minutes total; 13 minutes to present + 2 minutes for questions from the audience. Email me your slides as a pdf file before the class when you are presenting. Please find below some resources on how to give a good presentation.
3) Project update report (5 points, deadline: Oct 24 at 11:59pm local time): Write at most 1 page per student briefly describing your progress.
4) Final presentation (20 points, Nov 28, Dec 3, 5 in class): Present your project in class. One presentation per team. We will vote for the best project, which will get 10 bonus points. The exact format is yet to be determined.
5) Final report (50 points, deadline: Dec 13 at 11:59pm local time): Page limits for final reports listed under project types (double them if working as a team) exclude references and appendices, but note that appendices won’t influence grading and will be read at instructor’s discretion. It should be very clear from the report exactly who did what on the project! Please find below some resources on writing.
Notes: All written deliverables should be single-columned single-spaced with an 11 point font and 1 inch margins, and should be submitted as pdf files.
- Common Errors in Technical Writing, J. Owens
- Writing Technical Articles, H. Schulzrinne
- Common Bugs in Writing, H. Schulzrinne
- The Science of Scientific Writing, G. D. Gopen and J. A. Swan
- How to Write a Great Research Paper, S. P. Jones
- Academic Writing Check (automatically checks text for common pitfalls), D. Akhawe
- How to Present a Paper, L. Lamport
- How to Prepare for a Paper Presentation in a Seminar, S. Venkatasubramanian
- How to Give a Good Research Talk, S. P. Jones
- How to Give an Academic Talk, P. N. Edwards
- Presentation Zen: Simple Ideas on Presentation Design and Delivery, G. Reynolds
|Mon, Aug 20||Course Overview & Introduction||Lecture 1|
|Wed, Aug 22||Propositional Logic & SAT||
|Mon, Aug 27||First-Order Logic||Lecture 3|
|Wed, Aug 29||First-Order Theories I||Lecture 4|
|Mon, Sep 3||Labor Day|
|Wed, Sep 5||First-Order Theories II||
|Mon, Sep 10||Travel – SAS 2012 (Diego on SMT solvers)|
|Wed, Sep 12||Travel – SAS 2012 (Diego on SMT solvers)|
|Mon, Sep 17||Verification Conditions I||Lecture 6|
|Wed, Sep 19||Verification Conditions II||Lecture 7|
|Mon, Sep 24||Loops and Loop Invariants||
Homework 2 deadline
|Wed, Sep 26||Program Correctness: Strategies||
|Mon, Oct 1||Cancelled|
|Wed, Oct 3||Invariant Generation||
|Mon, Oct 8||Fall Break|
|Wed, Oct 10||Fall Break|
|Mon, Oct 15||Related Work Student Presentations|
|Wed, Oct 17||Related Work Student Presentations|
|Mon, Oct 22||Travel – Z3 Meeting (cancelled)|
|Wed, Oct 24||Travel – Z3 Meeting (Ganesh on termination)||Update report due|
|Mon, Oct 29||Related Work Student Presentations||Homework 3 deadline|
|Wed, Oct 31||Related Work Student Presentations|
|Mon, Nov 5||Symbolic Testing I||Lecture 11|
|Wed, Nov 7||Symbolic Testing II||Lecture 12|
|Mon, Nov 12||Automata Learning||Lecture 13|
|Wed, Nov 14||Checking Concurrent Programs I||
|Mon, Nov 19||Checking Concurrent Programs II||Lecture 15|
|Wed, Nov 21||Checking Concurrent Programs III|
|Mon, Nov 26||Predicate Abstraction||Lecture 16|
|Wed, Nov 28||Final Student Project Presentations|
|Mon, Dec 3||Final Student Project Presentations||Homework 4 deadline|
|Wed, Dec 5||Final Student Project Presentations|