CS6501 Machine Learning for Software Reliability (Fall 2025)


Logistics:

  • Instructor: Wenxi Wang (wenxiw@virginia.edu)
  • TA: Mingtian Tan (wtd3gz@virginia.edu)
  • Time: Tuesday & Thursday 9:30am - 11:45am
  • Location: Rice Hall 340
  • Office Hour: By appointment (Send us an email with the title starting with "CS6501 Office Hour Request")


Course Overview:
Building secure and reliable software systems is essential as modern society heavily relies on software for critical functions and daily operations. Formal reasoning provides a rigorous foundation for enhancing software reliability and security, while cutting-edge research leverages machine learning to improve the scalability and efficiency of these formal methods. This research-oriented course lies at the intersection of software engineering, formal methods, and machine learning. In general, this course contains two parts. In the first part, the course introduces fundamental concepts in software verification (including popular tools and techniques), formal reasoning (e.g., constraint solving), and machine learning (e.g., Graph Neural Networks, LLM, Reinforcement Learning). The second part focuses on interdisciplinary research, where students will read papers and undertake projects integrating these fields. External speakers may also be invited to give talks on relevant topics.


Prerequisites:
Graduate standing or permission from instructor. The students are expected to have basic knowledge of discrete math, data structures and algorithms, and to have considerable programming experience.


Grading:

  1. Quiz (5%): In the first part of the course, which focuses on basic concepts, it is important for students to read the mandatory reading materials. To ensure this, each lecture will begin with a 10-15 minute quiz containing two to three questions about the readings. The purpose of these quizzes is simply to check that students have completed the assigned readings.
  2. Paper Presentation (25%): (Signup Sheet): In each lecture in the second part of the course, one student will be tasked to present one or two papers selected for topic(s) he/she signed up for. The presentation duration for each paper is no less than 25 minutes and no more than 30 minutes, followed by a 5-10 minute question-and-answer session with the rest of the students. The presentation of a technical paper should at least include the following content:
    • The problem that the paper aims to address.
    • An overview of existing or related work, including state-of-the-art techniques previously applied to this problem.
    • The main contributions of the paper.
    • The methodology used in the paper and how it improves upon the current state-of-the-art.
    • An explanation of how the paper evaluates its proposed approach, including details on the experimental setup and evaluation metrics, etc.
    • The experimental results.
    • The limitations of the paper and potential directions for future research.
    The presentation of a survey paper should include the following:
    • Overview of the survey topic and its importance.
    • The main categories of the approaches in the existing literature.
    • Introduce the state-of-the art representative approaches in each category.
    • Key findings evaluation results for approaches in each category.
    • Strengths, weaknesses, and gaps in the current research.
    • Suggestions for future research areas.
    The presentation will be assessed based on the following criteria:
    • The presentation should have a clear and logical structure. The flow of information should be easy to follow, with each section building on the previous one.
    • Demonstrates a deep understanding of the paper’s content, including key concepts/ideas, methodologies, results, and conclusions.
    • Effectively explains complex ideas in a way that is accessible to the audience.
    • Encourages audience participation, effectively addresses questions raised by the audience, and engages in discussions.
    Deadline for slides submission: Send your slides to the instructor and TA via email at least 48 hours before your presentation (e.g., if presenting on Tuesday, slides should be submitted by Sunday 9:30 am). You will receive feedback from the instructor and TA to improve your slides, and if necessary, the instructor and TA may schedule a meeting with you to go over the slides. Late submissions after the deadline will result in a 50% presentation grade deduction.
  3. Participation (20%): For each lecture starting in the second part, everyone is required to complete the following two mini-assignments (regardless of whether or not you have signed up to present for that lecture):
    • Pre-lecture question: You are required to read at least the abstract and introduction of each paper to be presented in the lecture and submit at least one question for each paper you have after reading them. Your questions should be thoughtful and non-trivial (e.g., avoid questions like “Does the proposed method work?” or “What is the aim of the paper?”). You are also encouraged to bring up these questions during the 10-minute Q&A session in class. The deadline for submitting your questions is one day before the lecture (e.g., for Tuesday lectures, please submit your questions by Monday at 11:59 pm).
    • After attending the lecture, you are required to provide feedback to the presenters. Your feedback should address aspects such as clarity, completeness, and depth. It doesn’t need to be long, but it should be specific and constructive, aiming to help the presenters improve in the future. Please submit your feedback by 11:59 pm on the day of the presentation (to ensure it is fresh in your mind).
  4. Project (50%): By the end of this course, you must complete a research project, deliver a presentation on your findings, and submit a project report. While you are generally expected to lead your own project independently, you may choose to collaborate with a partner if you have a strong preference for teamwork. If you wish to work as a team, please discuss this with the instructor in advance. Be aware that the evaluation criteria for both the project report and presentation will be more rigorous for team projects. The project is not limited to the topics covered in the course, but it must focus on the intersection of Machine Learning, Software Engineering, and Formal Methods.
  5. The project grading breakdown (50%) is as follows: TBD

Late Submission Policy:
Assignments are expected to be submitted on time. Late submissions will be penalized as follows. Note that this late policy will not be applied to the presentation slides.

  • Up to 24 hours late: 10% deduction from the total assignment grade.
  • 24 to 48 hours late: 20% deduction from the total assignment grade.
  • 48 to 72 hours late: 30% deduction from the total assignment grade.
  • More than 72 hours late: Not accepted and will receive a grade of zero.

Extensions and Exceptions: Extensions will only be granted in exceptional circumstances, such as medical emergencies or other unforeseen, serious situations. If you need an extension, please contact me as soon as possible and provide appropriate documentation to support your request.

Grace Period: Each student is allowed one "grace period" per semester, where they can submit an assignment up to 24 hours late without penalty. This grace period does not require prior approval but must be requested within the first 24 hours after the deadline.


Schedule:
Note: This schedule is tentative and may be adjusted as the semester progresses.


Date Topic Contents Slides
8/26, Tue Introduction Logistics, Overview of the course overview
8/28, Thu No lecture, Reading N/A
Fundamental Knowledge in Formal Methods and Software Engineering
9/2, Tue Software Testing Guest Lecture:

Presenter: Pengyu Nie (Assistant Professor at University of Waterloo)

Readings:

  1. Differential Testing
  2. Metamorphic Testing
  3. Regression Testing (Chapter 3, starting from page 64)

Quiz before the lecture

 software testing
9/4, Thu SAT Solving

Readings:

  1. Classic Book: Decision Procedure by Daniel Kroening and Ofer Strichman (Read Chapter 1 and Chapter 2)
  2. Classic SAT solver MiniSat
  3. MiniSat page (optional)

Quiz before the lecture
9/9, Tue Software Modeling and Verification I

Readings:

  1. A popular software modeling tool, Alloy; read the Alloy tutorial
  2. Classic Book Reading: Software Abstractions by Daniel Jackson (optional)
  3. Alloy website (optional)

Quiz before the lecture
9/11, Thu Software Modeling and Verification II Guest Lecture:

Presenter: Chenyuan Yang (PhD at UIUC)

Readings:

  1. A recent popular verification tool called Verus: Verus paper
  2. Verus tutorial (optional)
  3. Rust programming language: Rust Book by Steve Klabnik, Carol Nichols, and Chris Krycho, with contributions from the Rust Community (optional)

Quiz before the lecture
9/16, Tue SOTA SAT Solving and SMT Solving

Part 1:
Guest Lecture:
Presenter: Armin Biere (Professor at Albert-Ludwigs-University Freiburg; Inventor of Kissat)
Content: Kissat

Part 2: SMT introduction

Readings:

  1. State-of-the-art SAT solver Kissat
  2. SMT Solving, read Decision Procedure, Chapter 3

Quiz before the lecture
Fundamental Knowledge in Machine Learning (especially for Software Engineering)
9/18, Thu Neural Networks Guest Lecture:

Presenter: Mingtian Tan (TA, PhD at UVA)

Readings:

  1. AlexNet, VGGNet, ResNet, and Inception
  2. Transformer
  3. Diffusion Model
  4. Graph Neural Networks

9/23, Tue Deep Learning Part 1: Guest Lecture:

Supervised, Unsupervised and Reinforcement Learning Introduction

Presenter: Mingtian Tan (TA, PhD at UVA)

Readings:

  1. Supervised Learning (Backpropagation)
  2. Unsupervised Learning (CLIP)
  3. Reinforcement Learning

9/25, Thu Large Language Model TBD
Research in the intersection of Machine Learning, Formal Methods and Software Engineering
9/30, Tue ML for SAT Solving
  • Paper 1:
  • Paper 2:
  • Optional Readings:
10/2, Thu Testing for ML
  • Paper 1:
  • Paper 2:
10/7, Tue Project Proposal Presentation
10/9, Thu LLM for Software Testing I
  • Paper 1:
  • Paper 2:
10/14, Tue No class, Fall Reading Days N/A
10/16, Thu LLM for Software Testing II
  • Paper 1:
  • Paper 2:
10/21, Tue LLM for Fuzzing
  • Paper 1:
  • Paper 2:
10/23, Thu LLM for Software Verification I
  • Paper 1:
  • Paper 2:
10/28, Tue LLM for Software Verification II
  • Paper 1:
  • Paper 2:
10/30, Thu LLM Safety
  • Paper 1:
  • Paper 2:
11/4, Tue No class, Election Day N/A
11/6, Thu LLM for Code Generation I
  • Paper 2:
  • Paper 1:
11/11, Tue LLM for Code Generation II
  • Paper 1:
  • Paper 2:
11/13, Thu Improving LLM Generated Code Quality
  • Paper 1:
  • Paper 2:
11/18, Tue LLM for Program Repair
  • Paper 1:
  • Paper 2:
  • Optional Readings:
11/20, Thu Fast and Slow Thinking Systems
  • Paper 1:
  • Paper 2:
11/25, Tue No class, Thanksgiving N/A
11/27, Thu No class, Thanksgiving N/A
12/2, Tue Final Project Presentation N/A
12/4, Thu Final Project Presentation N/A
12/9, Tue Project Final Report Due N/A


Students with disabilities or learning needs:
It is my goal to create a learning experience that is as accessible as possible. If you anticipate any issues related to the format, materials, or requirements of this course, please meet with me outside of class so we can explore potential options. Students with disabilities may also wish to work with the Student Disability Access Center (SDAC) to discuss a range of options to removing barriers in this course, including official accommodations. We are fortunate to have an SDAC advisor, Courtney MacMasters, physically located in Engineering. You may email her at cmacmasters@virginia.edu to schedule an appointment. For general questions please visit the SDAC website. If you have already been approved for accommodations through SDAC, please send me your accommodation letter and meet with me so we can develop an implementation plan together.

Religious accommodations:
It is the University's long-standing policy and practice to reasonably accommodate students so that they do not experience an adverse academic consequence when sincerely held religious beliefs or observances conflict with academic requirements.
Students who wish to request academic accommodation for a religious observance should submit their request to me by email as far in advance as possible. Students who have questions or concerns about academic accommodations for religious observance or religious beliefs may contact the University’s Office for Equal Opportunity and Civil Rights (EOCR) at UVAEOCR@virginia.edu or 434-924-3200.

Harassment, Discrimination, and Interpersonal Violence:
IThe University of Virginia is dedicated to providing a safe and equitable learning environment for all students. If you or someone you know has been affected by power-based personal violence, more information can be found on the UVA Sexual Violence website that describes reporting options and resources available.
The same resources and options for individuals who experience sexual misconduct are available for discrimination, harassment, and retaliation. UVA prohibits discrimination and harassment based on age, color, disability, family medical or genetic information, gender identity or expression, marital status, military status, national or ethnic origin, political affiliation, pregnancy (including childbirth and related conditions), race, religion, sex, sexual orientation, or veteran status. UVA policy also prohibits retaliation for reporting such behavior.
If you witness or are aware of someone who has experienced prohibited conduct, you are encouraged to submit a report to Just Report It or contact EOCR, the office of Equal Opportunity and Civil Rights.
If you would prefer to disclose such conduct to a confidential resource where what you share is not reported to the University, you can turn to Counseling & Psychological Services (“CAPS”) and Women’s Center Counseling Staff and Confidential Advocates (for students of all genders).
As your professor and as a person, know that I care about you and your well-being and stand ready to provide support and resources as I can. As a faculty member, I am a responsible employee, which means that I am required by University policy and by federal law to report certain kinds of conduct that you report to me to the University's Title IX Coordinator. The Title IX Coordinator's job is to ensure that the reporting student receives the resources and support that they need, while also determining whether further action is necessary to ensure survivor safety and the safety of the University community.

Support for your career development:
Engaging in your career development is an important part of your student experience. For example, presenting at a research conference, attending an interview for a job or internship, or participating in an external/shadowing experience are not only necessary steps on your path but are also invaluable lessons in and of themselves. I wish to encourage and support you in activities related to your career development. To that end, please notify me by email as far in advance as possible to arrange for appropriate accommodations.

Student support team:
You have many resources available to you when you experience academic or personal stresses. In addition to your professor, the School of Engineering and Applied Science has staff members located in Thornton Hall who you can contact to help manage academic or personal challenges. Please do not wait until the end of the semester to ask for help!

Learning:
Lisa Lampe, Assistant Dean for Undergraduate Affairs
Georgina Nembhard, Director of Student Success
Courtney MacMasters, Accessibility Specialist
Free tutoring is available for most classes.

Health and Wellbeing:
Kelly Garrett, Assistant Dean of Students, Student Safety and Support
Elizabeth Ramirez-Weaver, CAPS counselor*
Katie Fowler, CAPS counselor*

*You may schedule time with the CAPS counselors through Student Health. When scheduling, be sure to specify that you are an Engineering student. You are also urged to use TimelyCare for either scheduled or on-demand 24/7 mental health care.

Community and Identity:
The Center for Diversity in Engineering (CDE) is a student space dedicated to advocating for underrepresented groups in STEM. It exists to connect students with the academic, financial, health, and community resources they need to thrive both at UVA and in the world. The CDE includes an open study area, event space, and staff members on site. Through this space, we affirm and empower equitable participation toward intercultural fluency and provide the resources necessary for students to be successful during their academic journey and future careers.