Teaching : CS 6110 – Formal Methods in System Design | Spring 2015

Instructor: Zvonimir Rakamaric
Time:
Mondays, Wednesdays 3:00pm-4:20pm
Location:
MEB 3105
Office hours: Catch me after class; find me in my office; email me.
Mailing list: sv@list.eng.utah.edu (everyone enrolled must subscribe)

Disclaimer
The course will cover software verification techniques that made its way into industry practice, and provide students with hands-on experience using such techniques and tools.
This is a tentative course syllabus (based on how I taught this course back in 2012) 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 is not based around any specific programming language or embedded system.

Prerequisites
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.

Textbook
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.

Course Projects
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., SMACK, VCC, Frama-C, Dafny, Boogie). 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 (10 points, deadline: Feb 18 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) Final presentation (30 points, Apr 20, 22, 27 in class): Present your project in class. One presentation per team. We will vote for the best presentation, which will get 10 bonus points. The exact format is yet to be determined. Please find below some resources on how to give a good presentation.
3) Final report (50 points, deadline: May 3 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 will not 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.
4) Peer review of other students’ final reports (10 points, deadline: May 6 at 11:59pm local time): More information to follow.

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.

Writing advice:

Presentation advice:

Calendar (tentative):

Date Topic Notes
Mon, Jan 12 Course Overview & Introduction Lecture 1
Wed, Jan 14 Propositional Logic & SAT Lecture 2
Mon, Jan 19 Martin Luther King Jr. Day
Wed, Jan 21 First-Order Logic Lecture 3,
Homework 1
Mon, Jan 26 First-Order Theories I Lecture 4
Wed, Jan 28 First-Order Theories II Lecture 5,
Homework 1 deadline
Mon, Feb 2 Verification Conditions I Lecture 6
Wed, Feb 4 Project Ideas Roundtable
Mon, Feb 9 Travel – NSF (Ganesh on model checking)
Wed, Feb 11 Travel – NSF (Ganesh on MPI analysis)
Mon, Feb 16 Presidents’ Day
Wed, Feb 18 Verification Conditions II Lecture 7,
Project proposal due
Mon, Feb 23 Cancelled
Wed, Feb 25 Cancelled Homework 2
Mon, Mar 2 Loops Invariants; Program Correctness Strategies Lecture 8,
Lecture 9

Wed, Mar 4 Student project updates (my office) Homework 2 deadline
Mon, Mar 9 Symbolic Testing Lecture 10,
Homework 3
Wed, Mar 11 Symbolic Testing, Checking Concurrent Programs Lecture 11,
Lecture 12
Mon, Mar 16 Spring Break
Wed, Mar 18 Spring Break
Mon, Mar 23 Checking Concurrent Programs Lecture 13
Wed, Mar 25 Student project updates (my office) Homework 3 deadline
Mon, Mar 30 Checking Concurrent Programs
Wed, Apr 1 SMT Solvers Lecture 14
Mon, Apr 6 SMT Solvers
Wed, Apr 8 Student project updates (my office)
Mon, Apr 13 Predicate Abstraction Lecture 15
Wed, Apr 15 HOL Light (Alexey Solovyev)
Mon, Apr 20 HOL Light (Alexey Solovyev)
Wed, Apr 22 Final Student Project Presentations
Mon, Apr 27 Final Student Project Presentations

Comments are closed.