CS4720 Research in Program Analysis

Burcu Kulahcioglu Ozkan,   Arie van Deursen

TU Delft, Spring 2026/Q4

Course description:

This course provides a comprehensive introduction to the field of software analysis, a critical aspect of software development and maintenance. We will delve into both theoretical foundations and practical applications, learning how to analyze, understand, and improve software systems. This course explores a comprehensive set of techniques for software analysis, including practical formal methods, model checking, static and dynamic analysis, and other key approaches to evaluating and improving software systems. Through hands-on project, you will gain experience understanding and applying these techniques and presenting them using a scientific valid methodology.

Study goals:

At the end of this course, you will be able to:

1. Explain different software analysis approaches, such as model checking, static, and dynamic analyses.
2. Apply the software analysis techniques to sample programs.
3. Analyze the results of software analysis techniques in terms of their precision and computational performance.
4. Evaluate the performance of different software analysis techniques and compare their pros and cons.

Course organization

• 5 ECTS: You need to devote at least 140 hours of study for this course.
• In-class meetings: The course consists of 8 2-hour meetings.
• Assessment: Group Report (weighting 80%), Group Presentation and Participation (weighting 20%)
• Teams: The students are responsible to form teams and communicate them to the course TAs.

Teaching assistants

• Ege Berkay Gulcan
• Zahra Seyedghorban
• Luan Li

Course schedule:

The schedule of the presentations will be announced in the first week of lectures. The list of papers and the schedule is subject to small changes during the term.

Paper presentations:

Each presentation will consist of a presentation followed by a Q&A session.

Each paper will be presented by a team of two students, where both students are expected to participate in the presentation and the Q/A. The presentations will be graded individually, based on individual performance.

You are expected to read all the presented papers and actively participate in the Q&A discussions.

Tentative list of the papers to be presented and discussed:

• “Can LLMs transform natural language intent into formal method postconditions”, FSE’24

• “OSVBENCH: Benchmarking LLMs on specification generation tasks for operating system verification”, AAAI’26

• “SysMoBench: Evaluating AI on formally modeling complex real-world systems”, Arxiv’26

• “MutDafny: A mutation-based approach to assess Dafny specifications”, ICSE’26

• “Model checking distributed protocols in Must, OOPSLA’24

• “Model checking guided testing for distributed systems”, EuroSys’23

• “Greybox fuzzing of distributed systems”, CCS’23

• “Model-guided fuzzing of distributed systems”, OOPSLA’25

• “Formal model guided conformance testing for blockchains”, Arxiv’25

• “Smart casual verification of the confidential consortium framework”, NSDI’25

• “Validating traces of distributed programs against TLA+ specifications, SEFM’24

• “Trace validation of unmodified concurrent systems with OmniLink”, Arxiv’26

• “VeriPlan: Integrating formal verification and LLMs into end-user planning”, CHI’05

• “Runtime protocol refinement checking for distributed protocol implementations”, NSDI’25

• “AgentSpec: Customizable runtime enforcement for safe and reliable LLM agents”, ICSE’26

• “VeriGrey: Greybox Agent Validation”, ArXiv’26

Course projects:

TBA

Submit your project assignments via BrightSpace.

Contact and communication:

Assignment announcements and submissions will be made through BrightSpace.