Course Syllabus

• Learn how to express software specifications in formal logic,
• Use real-world verification tools,
• Design invariants, preconditions, and postconditions,
• Learn how to read verification papers efficiently,
• Apply verification to your own research area via a course project

This course provides hands-on experience with verification tools and introduces the mathematical foundations that make these tools work. Coding exercises will introduce tools ranging from property-based testing frameworks to proof assistants. Readings of classic and cutting-edge research papers will explore verification in depth.

Students will propose, complete, and present a course project. Projects must meet at least one of the following conditions:

• Apply verification to another research area (e.g., robotics, machine learning, human-centered computing)
• Advance the state-of-the-art in software verification research (e.g., improve an SMT solver on a class of problems)
• Replicate prior work in software verification (e.g., re-implement a known algorithm)

Students may work individually or in pairs on all aspects of the course. Groups of three or more are not permitted.

There is no required textbook.

There are no required materials / textbooks.

Recommended materials:

A paper notebook --- to set project milestones and track progress. See Canvas page: Guidelines: Lab Notebook.

We intend to provide Gitpod images so that you can complete homeworks online without installing any software. If you wish to install the software yourself, here are the required tools and languages:

Slides and lecture notes will appear in the Pages tab on Canvas: https://utah.instructure.com/courses/1213725/pages 

Discord:

• https://discord.gg/FnfhAAzRa6 

Email:

• blg@cs.utah.edu
• benjaminlgreenman@gmail.com (unofficial, just in case delivery to the utah address fails)

• Prof. Ben: TBD
• TA Dibri: TBD

or by appointment.

TA Queue: TBD

Course Staff CANNOT provide language-specific help on projects. If you chose a language, then part of your task is to navigate its documentation and developer community --- no matter how small they might be!

Final grades will be based on:

• 15% for Coding Assignments, split across 5 assignments during the beginning of the course.
• 20% for written summaries of course Readings, split across TODO papers.
• 60% for your Term Project, split across 2 checkpoints and 4 final deliverable items:
  • Checkpoints: Project Proposal & Mid-Term Presentation
  • Deliverables: Written Report & Final Presentation & Codebase & Lab Notebook
• 5% for Quizzes and Surveys

Project proposals will be due in mid-February.

Letter grade policy for grad students (CS 6110):

Letter grade policy for undergrads (CS 5110):

The instructor reserves the right to adjust letter grades upward or downward on a case-by-case basis to reflect students' actual performance in the class.

Attendance: Class attendance is optional. If present, you will be expected to speak and to participate in class activities.

Zoom: Lectures will be streamed on zoom and recordings will be available on Canvas for several weeks. Zoom attendance is allowed but not encouraged. We will not monitor the zoom chat. We will not allow audio from participants. The positioning of the recording camera and microphone may be poor. Our goal with the recordings is to allow anyone to catch up with class for any reason it might be necessary, no questions asked, but without distractions for in-person participants.

Academic Misconduct: We follow the Kahlert School of Computing policy. See below. Academic dishonesty results in a failing grade for the course. Two instances of academic dishonestly lead to expulsion from the major. 

Collaboration: Working in pairs is allowed on coding assignments and the term project. Email the professor to create a pair. Pairs should submit one deliverable on Canvas (if you submit two, we will choose one submission to grade). Email the instructor to break up a pair.

AI + LLM: You may use LLMs such as ChatGPT for any part of the course, but you must cite the LLM's contribution to your submission and you must take ownership of the work. For example, it would be bad to use an LLM to produce your entire final project if you are unable to relate the output to research on software verification. When in doubt, ask the instructor. Be advised that AI tools such as ChatGPT, DeepSeek, etc. may produce wrong and misleading outputs, and that their cost to the environment may not be factored into their usage price.

• U. Utah Center for Teaching Excellence AI guidelines: https://cte.utah.edu/instructor-education/ai-for-teaching.php 

Accommodations will be considered on an individual basis and may require documentation.

Please contact the instructor as soon as possible (preferably shortly before the semester begins) to request accommodations of any kind.

Contact your instructor as soon as possible if an extreme personal circumstance
(hospitalization, death of a close relative, natural disaster, etc.) is interfering with your ability to
complete your work.

To request an accommodation for religious practices, contact your instructor at the beginning of the semester.

If you are student on active duty with the military and experience issues that prevent you from participating in the course because of deployment or service responsibilities, contact your instructor as soon as possible to discuss appropriate accommodations.