CS6501 Machine Learning for Software Reliability (Fall 2024)


Logistics:

  • Instructor: Wenxi Wang (wenxiw@virginia.edu)
  • TA: Mingtian Tan (wtd3gz@virginia.edu)
  • Time: Mondays & Wednesdays 11:00am - 12:15pm
  • Location: Rice Hall 011
  • 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 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 two papers selected for topic(s) he/she signed up for. The presentation duration for each student 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 Monday, slides should be submitted by Saturday 11:00 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 Monday lectures, please submit your questions by Sunday 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:
    • Project proposal presentation (Deadline: 10/9 in class Guideline) and project proposal (Deadline: 10/15 11:59 pm; Guideline): 15%
    • Final presentation (Deadline: 11/25 and 12/2 in class Guideline ) and final report (Deadline: 12/9 11:59 pm; Guideline ): 35%

Thanks Yu Meng for his suggestions in the grading instructions.


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/28, Wed Introduction Logistics, Overview of the course overview
9/2, Mon No lecture, Travel N/A
Fundamental Knowledge in Formal Methods and Software Engineering
9/4, Wed Symbolic Execution Guest Lecture:

Presenter: Yang Hu (Applied Scientist in AWS, PhD in UT Austin)

Readings:

  1. Symbolic execution slides by Michael Hicks
  2. KLEE, a famous symbolic execution tool
  3. KLEE webpage (optional)

Quiz before the lecture

 symbolic execution
9/9, Mon SAT Solving I

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

 sat
9/11, Wed SAT Solving II 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
  • kissat
  • smt
    • 9/16, Mon Software Modeling and Verification

    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/18, Wed Software Testing Guest Lecture:

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

    Readings:

    1. Differential Testing
    2. Metamorphic Testing
    3. Regression Testing

    Quiz before the lecture

    		 testing
    Fundamental Knowledge in Machine Learning (especially for Software Engineering)
    9/23, Mon 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

    		nn_models
    9/25, Wed Deep Learning Part 1: Guest Lecture:

    Supervised and Unsupervised Learning Introduction Presenter: Mingtian Tan (TA, PhD at UVA)

    Part 2: GNN and Reinforcement Learning Introduction

    Readings:

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

  • learning
  • gnn_rl
    • 9/30, Mon Large Language Model Guest Lecture:

    Presenter: Yuxiang Wei (PhD at UIUC)

    Readings:

    1. Magicoder: Empowering Code Generation with OSS-Instruct
    2. Copiloting the Copilots: Fusing Large Language Models with Completion Engines for Automated Program Repair
    3. Automated Program Repair in the Era of Large Pre-trained Language Models

    		llm4code
    Research in the intersection of Machine Learning, Formal Methods and Software Engineering
    10/2, Wed ML for SAT Solving rishov_slides
    10/7, Mon Testing for ML
    10/9, Wed Project Proposal Presentation Schedule
    10/14, Mon No class, Fall Reading Days N/A
    10/16, Wed LLM for Software Testing I
    10/21, Mon LLM for Software Testing II
    10/23, Wed LLM for Fuzzing
    10/28, Mon LLM for Software Verification I
    10/30, Wed LLM for Software Verification II
    11/4, Mon LLM Safety
    11/6, Wed LLM for Code Generation I
    11/11, Mon LLM for Code Generation II
    11/13, Wed Improving LLM Generated Code Quality
    11/18, Mon LLM for Program Repair
    11/20, Wed Fast and Slow Thinking Systems
    11/25, Mon Final Project Presentation N/A
    11/27, Wed No lecture, Thanksgiving N/A
    12/2, Mon Final Project Presentation N/A
    12/9, Wed 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.