CS 6110-001 Spring 2024 Software Verification
Syllabus
CS 5110/6110 Software Verification
WEB L112 TR 14:00-15:20
(livestreamed and recorded via Zoom)
Instructors
| Instructor: |
Ben Greenman <blg@cs.utah.edu> MEB 3252 |
| Teaching Assistant: |
Suyasha Bobhate <help-cs6110@lists.utah.edu> |
Course Description
Overview
| Course | CS 5110/6110 |
| Department | School of Computing |
| Pre-Requisites (5110) |
CS 3100, 3505, 4150 |
| Credit Hours | 3 |
| Semester | Fall 2024 |
| Outcomes | Learn how to: * translate software specifications into logic, * use real-world verification tools, * design invariants and pre/post conditions, * efficiently read verification papers, * and apply verification to your research area (via a course project). |
Goals & Objectives
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.
Materials
There are no required materials / textbooks.
Recommended materials:
- A paper notebook --- to set project milestones and track progress. See Guidelines: Lab Notebook.
We intend to provide Gitpod images so that you can complete homeworks online without installing any software. But if you wish to install the software yourself (maybe for speed or to use emacs), here are the requirements:
Communication
The best way to reach the instructors is via email. Use any of the following:
- help-cs6110@lists.utah.edu
- blg@cs.utah.edu
- Canvas the Inbox, located in the far left Canvas menu.
The course has a Discord for lightweight communication with the instructors and other students. Try the invite link below, or contact the instructor for access:
Office Hours
The instructor will hold hours after class and by appointment. The TAs will hold the hours listed below.
| Monday | 3:00pm - 4:00pm | MEB 3145 | Suyasha |
| Tuesday | 3:30pm - 4:30pm | MEB 3252 | Ben |
| Wednesday | 3:00pm - 4:00pm | MEB 3145 | Suyasha |
| Thursday | 3:30pm - 4:30pm | MEB 3252 | Ben |
- Course Staff CANNOT provide language-specific help on projects.
- If you chose a tool/language, then part of your task is to navigate its documentation and developer community --- no matter how small they are!
Evaluation
- 15% Coding Homework
- split across 5 assignments during the first few weeks of the course
- 20% Paper Readings
- split across approximately 10 readings
- 60% Course Project
- split across 4 final deliverables and 2 intermediate checkpoints:
- deliverables: written report, 10min presentation, codebase, and lab notebook
- checkpoints: initial proposal, 2min mid-term presentation
- EDIT 02/27: removed version history deliverable, replaced mid-term meeting with short presentation
- split across 4 final deliverables and 2 intermediate checkpoints:
- 5% Quizzes and Surveys
Project proposals will be due in mid-February.
Tentative letter grade policy for graduate students:
| 100-93 A | 89-87 B+ | 79-77 C+ | 69-67 D+ | 59-0 E |
| 92-90 A- | 86-83 B | 76-73 C | 66-63 D | |
| 82-80 B- | 72-70 C- | 62-60 D- |
Tentative letter grade policy for undergraduates:
| 100-90 A | 86-83 B+ | 76-73 C+ | 66-63 D+ | 56-0 E |
| 89-87 A- | 82-80 B | 72-70 C | 62-60 D | |
| 79-77 B- | 69-67 C- | 59-57 D- |
Course Policies
- Submit assignments on Canvas
- Late submissions are accepted any time, but will be penalized roughly 10% per day (subject to instructor discretion)
- Working in pairs is allowed, subject to the following conditions:
- Ask the professor to create a pair (in person or via email)
- Pairs may submit at most one deliverable on Canvas
- If students A and B are working together, then either A or B should submit. If both submit, then the course staff will discard one of the submissions arbitrarily.
- Pairs cannot break up without permission from the professor, but anyone can request a breakup at any time.
- 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 professor!
- Beware that LLMs:
- are NOT an acceptable source of information on course policies,
- may output text that is incorrect or misleading, and
- may have a large cost to the environment that is not fully accounted for.
Support
Accommodations will be considered on an individual basis and may require documentation.
Please contact your instructor and/or teaching assistant 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.
Disability Access
All written information in this course can be made available in an alternative format with prior notification to the Center for Disability Services (CDS). CDS will work with you and the instructor to make arrangements for accommodations. Prior notice is appreciated. To read the full accommodations policy for the University of Utah, please see Section Q of the Instruction & Evaluation regulations.
If you will need accommodations in this class, contact:
Center for Disability Services
801-581-5020
disability.utah.edu
162 Union Building
200 S. Central Campus Dr.
Salt Lake City, UT 84112
Office of Equal Opportunity
The Office of Equal Opportunity And Affirmative Action (OEO/AA) is dedicated to providing a fair and equitable environment for all to pursue their academic and professional endeavors and to equally access University programs.
OEA/AA
801-581-8365
oeo.utah.edu
383 South University Street
Level 1, OEO Suite
Salt Lake City, UT 84112
Price College Counseling Service
Goal: provide a confidential, safe, and non-judgmental space to address any stressor or concern in your life. Empower you to take actions to meet your needs, values, and goals.
Call to schedule an Initial Consultation (IC) appointment. Be sure to ask for “embedded counseling for College of Engineering”.
Counseling Center
801-581-6826
www.price.utah.edu/students/current/counseling
WEB 1707
University Policies
COVID-19 Information
Drop/Withdrawal Policies
Students may drop a course within the first two weeks of a given semester without any penalties.
Students may officially withdraw (W) from a class or all classes after the drop deadline through the midpoint of a course. A “W” grade is recorded on the transcript and appropriate tuition/fees are assessed. The grade “W” is not used in calculating the student’s GPA.
For deadlines to withdraw from full-term, first, and second session classes, see the U's Academic Calendar.
Academic Honesty, Plagiarism and Cheating
It is assumed that all work submitted to your instructor is your own work. When you have used the ideas of others, you must properly indicate that you have done so.
It is expected that students adhere to University of Utah policies regarding academic honesty, including but not limited to refraining from cheating, plagiarizing, misrepresenting one’s work, and/or inappropriately collaborating. This includes the use of generative artificial intelligence (AI) tools without citation, documentation, or authorization. Students are expected to adhere to the prescribed professional and ethical standards of the profession/discipline for which they are preparing. Any student who engages in academic dishonesty or who violates the professional and ethical standards for their profession/discipline may be subject to academic sanctions as per the University of Utah’s Student Code: https://regulations.utah.edu/academics/6-410.php
Plagiarism and cheating are serious offenses and may be punished by failure on an individual assignment, and/or failure in the course. Academic misconduct, according to the University of Utah Student Code,
“...Includes, but is not limited to, cheating, misrepresenting one’s work, inappropriately collaborating, plagiarism, and fabrication or falsification of information…It also includes facilitating academic misconduct by intentionally helping or attempting to help another to commit an act of academic misconduct.”
For details on plagiarism and other important course conduct issues, see the U's Code of Student Rights and Responsibilities.
Course Materials Copyright
Sale or distribution of information representing the work product of a faculty member to a commercial entity for financial gain without the express written permission of the faculty member responsible for the course. (“Work product” means original works of authorship that have been fixed in a tangible medium and any works based upon and derived from the original work of authorship.)
Safety at the U
The University of Utah values the safety of all campus community members. You will receive important emergency alerts and safety messages regarding campus safety via text message.
For more safety information and to view available training resources, including helpful videos, visit safeu.utah.edu (Links to an external site.).
To report suspicious activity or to request a courtesy escort, contact:
Campus Police & Department of Public Safety
801-585-COPS (801-585-2677)
dps.utah.edu
1735 E. S. Campus Dr.
Salt Lake City, UT 84112
Wellness at the U
Your personal health and wellness are essential to your success as a student. Personal concerns like stress, anxiety, relationship difficulties, depression, or cross-cultural differences can interfere with a student’s ability to succeed and thrive in this course and at the University of Utah.
Please feel welcome to reach out to your instructor or TA to handle issues regarding your coursework.
For helpful resources to manage your personal wellness and counseling options, contact:
Center for Student Wellness
801-581-7776
wellness.utah.edu
2100 Eccles Student Life Center
1836 Student Life Way
Salt Lake City, UT 84112
Women's Resource Center
801-581-8030
womenscenter.utah.edu
411 Union Building
200 S. Central Campus Dr.
Salt Lake City, UT 84112
Addressing Sexual Misconduct
Title IX makes it clear that violence and harassment based on sex and gender (which includes sexual orientation and gender identity/expression) is a civil rights offense subject to the same kinds of accountability and the same kinds of support applied to offenses against other protected categories such as race, national origin, color, religion, age, status as a person with a disability, veteran’s status, or genetic information.
If you or someone you know has been harassed or assaulted, you are encouraged to report it to university officials:
Title IX Coordinator & Office of Equal Opportunity and Affirmative Action
801-581-8365
oeo.utah.edu
383 South University Street
Level 1 OEO Suite
Salt Lake City, UT 84112
Office of the Dean of Students
801-581-7066
deanofstudents.utah.edu
270 Union Building
200 S. Central Campus Dr.
Salt Lake City, UT 84112
To file a police report, contact:
Campus Police & Department of Public Safety
801-585-COPS (801-585-2677)
dps.utah.edu
1658 E 500 S
Salt Lake City, UT 84112
If you do not feel comfortable reporting to authorities, the U's Victim-Survivor Advocates provide free, confidential, and trauma-informed support services to students, faculty, and staff who have experienced interpersonal violence.
To privately explore options and resources available to you with an advocate, contact:
Center for Campus Wellness
801-581-7776
wellness.utah.edu
Student Services Building (SSB)
Room 330
201 S. 1460 E.
Salt Lake City, UT 84112
Americans With Disabilities Act (ADA)
The University of Utah seeks to provide equal access to its programs, services, and activities for people with disabilities.
All written information in this course can be made available in an alternative format with prior notification to the Center for Disability & Access (CDA). CDA will work with you and the instructor to make arrangements for accommodations. Prior notice is appreciated. To read the full accommodations policy for the University of Utah, please see Section Q of the Instruction & Evaluation regulations.
If you will need accommodations in this class, or for more information about what support they provide, contact:
Center for Disability & Access
801-581-5020
disability.utah.edu
162 Union Building
200 S. Central Campus Dr.
Salt Lake City, UT 84112
Diverse Student Support
Your success at the University of Utah is important to all of us here! If you feel like you need extra support in academics, overcoming personal difficulties, or finding community, the U is here for you.
Student Support Services (TRIO)
TRIO federal programs are targeted to serve and assist low-income individuals, first-generation college students, and individuals with disabilities.
Student Support Services (SSS) is a TRIO program for current or incoming undergraduate university students who are seeking their first bachelor's degree and need academic assistance and other services to be successful at the University of Utah.
For more information about what support they provide, a list of ongoing events, and links to other resources, view their website or contact:
Student Support Services (TRIO)
801-581-7188
trio.utah.edu
Room 2075
1901 E. S. Campus Dr.
Salt Lake City, UT 84112
American Indian Students
The AIRC works to increase American Indian student visibility and success on campus by advocating for and providing student-centered programs and tools to enhance academic success, cultural events to promote personal well-being, and a supportive “home-away-from-home” space for students to grow and develop leadership skills.
For more information about what support they provide, a list of ongoing events, and links to other resources, view their website or contact:
American Indian Resource Center
801-581-7019
diversity.utah.edu/centers/airc
Fort Douglas Building 622
1925 De Trobriand St.
Salt Lake City, UT 84113
Black Students
Using a pan-African lens, the Black Cultural Center seeks to counteract persistent campus-wide and global anti-blackness. The Black Cultural Center works to holistically enrich, educate, and advocate for students, faculty, and staff through Black-centered programming, culturally affirming educational initiatives, and retention strategies.
For more information about what support they provide, a list of ongoing events, and links to other resources, view their website or contact:
Black Cultural Center
801-213-1441
diversity.utah.edu/centers/bcc
Fort Douglas Building 603
95 Fort Douglas Blvd.
Salt Lake City, UT 84113
Students with Children
Our mission is to support and coordinate information, program development, and services that enhance family resources as well as the availability, affordability, and quality of child care for University students, faculty, and staff.
For more information about what support they provide, a list of ongoing events, and links to other resources, view their website or contact:
Center for Childcare & Family Resources
801-585-5897
childcare.utah.edu
408 Union Building
200 S. Central Campus Dr.
Salt Lake City, UT 84112
Students With Disabilities
The Center for Disability and Access is dedicated to serving students with disabilities by providing the opportunity for success and equal access at the University of Utah. They also strive to create an inclusive, safe, and respectful environment.
For more information about what support they provide and links to other resources, view their website or contact:
Center for Disability and Access
801-581-5020
disability.utah.edu
162 Union Building
200 S. Central Campus Dr.
Salt Lake City, UT 84112
Students of Ethnic Descent
The Center for Ethnic Student Affairs offers several programs dedicated to the success of students with varied cultural and ethnic backgrounds. Its mission is to create an inclusive, safe campus community that values the experiences of all students.
For more information about what support they provide, a list of ongoing events, and links to other resources, view their website or contact:
Center for Ethnic Student Affairs
801-581-8151
diversity.utah.edu/centers/cesa/
235 Union Building
200 S. Central Campus Dr.
Salt Lake City, UT 84112
English as a Second/Additional Language (ESL) Students
If you are an English language learner, there are several resources on campus available to help you develop your English writing and language skills. Feel free to contact:
Writing Center
801-587-9122
writingcenter.utah.edu
(Links to an external site.)
2701 Marriott Library
295 S 1500 E
Salt Lake City, UT 84112
English for Academic Success (EAS) Program
801-581-8047
linguistics.utah.edu
2300 LNCO
255 S. Central Campus Dr.
Salt Lake City, UT 84112
English Language Institute
801-581-4600
continue.utah.edu/eli (Links to an external site.)
540 Arapeen Dr.
Salt Lake City, UT 84108
Undocumented Students
Immigration is a complex phenomenon with broad impact—those who are directly affected by it and those who are indirectly affected by their relationships with family members, friends, and loved ones. If your immigration status presents obstacles that prevent you from engaging in specific activities or fulfilling specific course criteria, confidential arrangements may be requested from the Dream Center.
Arrangements with the Dream Center will not jeopardize your student status, your financial aid, or any other part of your residence. The Dream Center offers a wide range of resources to support undocumented students (with and without DACA) as well as students from mixed-status families.
For more information about what support they provide and links to other resources, view their website or contact:
Dream Center
801-213-3697
dream.utah.edu
(Links to an external site.)
200 S. CENTRAL CAMPUS DRIVE
UNION, ROOM 80
SALT LAKE CITY, UT 84112
LGBTQ+ Students
The LGBTQ+ Resource Center acts in accountability with the campus community by identifying the needs of people with a queer range of [a]gender and [a]sexual experiences and responding with university-wide services.
For more information about what support they provide, a list of ongoing events, and links to other resources, view their website or contact:
LGBTQ+ Resource Center
801-587-7973
lgbt.utah.edu (Links to an external site.)
409 Union Building
200 S. Central Campus Dr.
Salt Lake City, UT 84112
Veterans & Military Students
The mission of the Veterans Support Center is to improve and enhance the individual and academic success of veterans, service members, and their family members who attend the university; to help them receive the benefits they earned, and to serve as a liaison between the student veteran community and the university.
For more information about what support they provide, a list of ongoing events, and links to other resources, view their website or contact:
Veterans Support Center
801-587-7722
veteranscenter.utah.edu (Links to an external site.)
418 Union Building
200 S. Central Campus Dr.
Salt Lake City, UT 84112
Women
The Women’s Resource Center (WRC) at the University of Utah serves as the central resource for educational and support services for women. Honoring the complexities of women’s identities, the WRC facilitates choices and changes through programs, counseling, and training grounded in a commitment to advance social justice and equality.
For more information about what support they provide, a list of ongoing events, and links to other resources, view their website or contact:
Women's Resource Center
801-581-8030
womenscenter.utah.edu
411 Union Building
200 S. Central Campus Dr.
Salt Lake City, UT 84112
Inclusivity at the U
The Office for Inclusive Excellence is here to engage, support, and advance an environment fostering the values of respect, diversity, equity, inclusivity, and academic excellence for students in our increasingly global campus community. They also handle reports of bias in the classroom as outlined below:
Bias or hate incidents consist of speech, conduct, or some other form of expression or action that is motivated wholly or in part by prejudice or bias whose impact discriminates, demeans, embarrasses, assigns stereotypes, harasses, or excludes individuals because of their race, color, ethnicity, national origin, language, sex, size, gender identity or expression, sexual orientation, disability, age, or religion.
For more information about what support they provide and links to other resources, or to report a bias incident, view their website or contact:
Office for Inclusive Excellence
801-581-4600
inclusive-excellence.utah.edu (Links to an external site.)
200 S. CENTRAL CAMPUS DRIVE
UNION, ROOM 70
SALT LAKE CITY, UT 84112
Other Student Groups at the U
To learn more about some of the other resource groups available at the U, check out:
The syllabus page shows a table-oriented view of the course schedule, and the basics of course grading. You can add any other comments, notes, or thoughts you have about the course structure, course policies or anything else.
To add some comments, click the "Edit" link at the top.