CS 6110-001 Spring 2017 Rigorous System Design

Course Name: CS 5110/6110 - Rigorous System Design

Class Meetings: 3:40-5:00, Tuesdays and Thursdays in MEB 2325

Instructor: Zvonimir Rakamaric
Email: zvonimir@cs.utah.edu (only for urgent private matters, otherwise message me on canvas)
Office: MEB 3424
Office Hours: Catch me after class; find me in my office; message me

Teaching Assistant: Shaobo He
Contact: message me on canvas
Office: MEB 3167
Office Hours: 5:00-6:00 on Tuesdays and 9:30-10:30 on Wednesdays

Course Description and Objective
The main goal of the course is to teach students how to prove programs and systems 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 50% homework assignments and 50% course project. There will be 5-6 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.
The letter grading policy for graduate students is as follows:

For undergraduate students, the grading policy is as follows:

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 for postponing your submission.

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. A common example of cheating (in the form of plagiarism) is copy-pasting text from other sources into your report as your own, i.e., without putting it into quotation marks.

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 7 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 7 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 14 pages).

If you have an idea for a project that does not fit into any of  the listed categories, come and talk to me and I will try to accommodate it. If you don’t have an idea for a project, stop by my office and we will 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 ideas (2 points, deadline: Feb 14 at 3:40pm local time): Write a short paragraph or simple bullet-points listing project ideas that you thought about and are interested in. Listing half-baked ideas is totally fine. I would just like to see that you gave this some thought.
2) Project proposal (8 points, deadline: Feb 23 at 3:40pm 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.
3) Final presentation (30 points, deadline: Apr 18 at 3:40pm local time, presenting on Apr 20 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.
4) Final report (50 points, deadline: Apr 26 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.
5) Peer review of other students’ final reports (10 points, deadline: Apr 30 at 11:59pm local time): You will be assigned two project reports by other students to review. I am expecting that you will write a brief review (one paragraph) for each of the two reports that you get assigned. Reviews are anonymous. Still, you should of course be kind and offer constructive criticism when needed. Make sure to critically comment on the project outcomes. Are the goals and motivation of the project clear? Is it clear what was actually achieved? Is empirical evaluation satisfactory? Is the report properly structured and well-written?

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:

• 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