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.
    Presentation Slides: We encourage you to send your slides to the instructor 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 to improve your slides, and if necessary, the instructor may schedule a meeting with you to go over the slides.
  3. Participation (20%): For each lecture starting in the second part, everyone (except the presenter) is required to complete the following mini-assignments:
    • 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:
    • project proposal (Deadline: 10/14 11:59 pm; Guideline): 15%

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

 CDCL SAT
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
  • Alloy
  • demo
    • 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

    		 Verus
    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 Guest Lecture:

    Presenter: Trey Woodlief (Assistant Professor at William & Mary)

    Readings:

    1. ScenicNL: Generating Probabilistic Scenario Programs from Natural Language
    2. ODD-diLLMma: Driving Automation System ODD Compliance Checking using LLMs
    3. MOSU: Autonomous Long-range Robot Navigation with Multi-modal Scene Understanding

    		LLM for ADS
    Research in the intersection of Machine Learning, Formal Methods and Software Engineering
    9/30, Tue Topic 1: Software Verification for ML models
  • TrainVerify - Kahfi Zulkifli
  • Mirage - John Berberian
    • 10/2, Thu Topic 2: LLM for Software Verification
  • KNighter - Dimas Parikesit
  • FSCQ - Shaina Kumar
    • 10/7, Tue Topic 3: Improving LLM Reasoning
  • Paper 1: GraphReason: Enhancing Reasoning Capabilities of Large Language Models through A Graph-Based Verification Approach
  • Paper 2: DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning
    • 10/9, Thu Project Proposal Discussion N/A
    10/14, Tue No class, Fall Reading Days N/A
    10/16, Thu Topic 4: Neurosymbolic AI - I
    10/21, Tue Topic 5: Neurosymbolic AI - II
    10/23, Thu Topic 6: LLM for Code Generation - I
    10/28, Tue Topic 7: LLM for Code Generation - II
    • Paper 1:
    • Paper 2:
    10/30, Thu Topic 8: LLM for Software Testing
    11/4, Tue No class, Election Day N/A
    11/6, Thu Topic 9: LLM for fuzzing
    11/11, Tue Topic 10: RL for SE
    11/13, Thu Topic 11: LLM for Proof Generation
    11/18, Tue Topic 12: Trustworthy AI
    11/20, Thu Topic 13: Fast and Slow Thinking Systems
    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 Final Project Presentation 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.