Link

CS4720 Research in Program Analysis

Burcu Kulahcioglu Ozkan,   Arie van Deursen

Spring 2025/Q4, TU Delft

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

Teaching assistants

Course schedule:

Week-1 April 22
Introduction to Software Analysis
  • Lecture: Introduction to the course
  • Lecture: Static vs dynamic software analysis
Further reading:

Actions and assignments (due April 28th):

  • Select your team members
  • Select your paper to present (paper selection is first-come-first-served)
Note: If the teams/papers are not selected by the deadline, they will be assigned randomly.
Week-2 April 29
Introduction to Model Checking
  • Lecture: Introduction to model checking
  • Lecture: Introduction to model checking with TLA+ (hands on, bring your computers) (Lecturer: Ege Berkay Gulcan)

Further reading:

Actions and assignments (due May 6th):

  • Check-in with your team
  • Kick-the-tires for your paper presentation
  • Read the research papers of week-3 and prepare for the discussion
Week-3 May 6
Model Checking of Software
  • Lecture: Software model checking

Further reading:

Paper presentations (model checking):

Actions and assignments (due May 12th):

  • Select your course project
  • Read the research papers of week-4 and prepare for the discussion
Note: If a team does not select a project by the deadline, their project will be assigned randomly.
Week-4 May 13
From Model Checking to Concurrency Testing
  • Lecture: Introduction to concurrency testing

Further reading:

Paper presentations (concurrency testing):

Actions and assignments:

  • Kick-the-tires for your project (due May 19)
  • Read the research papers of week-6 and prepare for the discussion (due May 27)
Week-5 May 20
No lectures
Week-6 May 27
Concurrency Testing at JetBrains
Guest lecture by Nikita Koval and Bob Brockbernd
  • Lecture: Testing concurrent data structures on JVM

Further reading:

Actions and assignments (due June 3rd):

  • Read the research papers of week-7 and prepare for the discussion
Week-7 June 3
Fault-Injection Testing
  • Lecture: Probabilistic concurrency testing
  • Lecture: Introduction to fault-injection testing

Further reading:

Paper presentations (concurrency testing):

Actions and assignments (due June 10th):

  • Read the research papers of week-7 and prepare for the discussion
Week-8 June 10
More on Concurrency anf Fault-Injection Testing
Paper presentations (concurrency and fault-injection testing):

Actions and assignments (due June 17th):

  • In-progress project submissions (in-progress project report + code)
Week-9 June 17
No lectures

Actions and assignments (due June 24th):

  • Final project submissions (project report + code)
Week-10 June 24
Final project presentations (5 min presentation + 5 min Q/A)

The schedule is subject to small changes during the term.

Lecture notes:

Please find the lecture notes on the BrightSpace.

Assignment submissions:

Submit your assignments via BrightSpace.

Paper presentations:

Each presentation will have a 20-minute slot, consisting of a 10-minute presentation followed by a 10-minute 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 discussion for each one.

Course projects:

TBA

Contact and communication:

Assignment announcements and submissions will be made through BrightSpace.

You can also enroll in the course Mattermost channel to connect to your peers and faster discussion.