Course Syllabus

Course Name: CS 5110/6110 - Software Verification

Class Meetings: 1:25-2:45, Mondays and Wednesdays in WEB L122

Instructor: Zvonimir Rakamarić
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

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.

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:

Inclusivity. It is my intent that students from all diverse backgrounds and perspectives be well-served by this course, that students' learning needs be addressed both in and out of class, and that the diversity that the students bring to this class be viewed as a resource, strength, and benefit. It is my intent to present materials and activities that are respectful of diversity: gender identity, sexuality, disability, age, socioeconomic status, ethnicity, race, nationality, religion, and culture.
I also except students to treat others in the class, including the teaching staff, with the same level of respect.
Your suggestions on how we can make the course more inclusive and welcoming are encouraged and appreciated. You can give me feedback in person or via email.
I take incidents of discrimination, bias, and harassment seriously. I will file reports with the Office or Equal Opportunity, Affirmative Action, and Title IX (OEO) about such incidents. If you are unsure what differentiates free speech and profession behavior from discrimination, bias, and harassment, I am happy to have an open, judgement-free, and confidential conversation with you, or refer you to the OEO.
More resources:
U of U Inclusivity Statement
Center for Ethnic Student Affairs
LGBT Resource Center
American Indian Resource Center
Office of Equal Opportunity, Affirmative Action, and Title IX
Center for Student Wellness

Student Name and Personal Pronoun. Class rosters are provided to the instructor with the student’s legal name as well as “Preferred first name” (if previously entered by you in the Student Profile section of your CIS account). While CIS refers to this as merely a preference, I will honor you by referring to you with the name and pronoun that feels best for you in class, on papers, exams, group projects, etc. Please advise me of any name or pronoun changes (and please update CIS) so I can help create a learning environment in which you, your name, and your pronoun will be respected.

Policies and Academic Misconduct. Please read the School of Computing Policies and Guidelines and College of Engineering Guidelines. In particular, make sure to read the Policy Statement on 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 1:25pm 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. Make sure to list 2-3 potential project ideas.
2) Project proposal (8 points, deadline: Feb 28 at 1:25pm local time): Write 2-3 pages per team describing your project plan. Absolutely make sure you discuss your project idea with me at least a week before the proposal due date. The proposal should include:

• Project title, list of team members
• Statement of the problem to be investigated, and an explanation of why the problem is interesting
• Description of what you propose to do
• Explain the experiments you plan to perform (if any), and what you hope to show with your empirical evaluation; describe what your benchmarks will be and where you will obtain them. If you do not plan to undertake an empirical evaluation, clarify why it is not needed.
• List basic milestones and tasks with deadlines
• Short description of related work

3) Final presentation (30 points, deadline: Apr 18 at 1:25pm local time, presenting on Apr 23 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 25 at 08:00am 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 28 at 08:00am 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