Overview

This course provides an overview of techniques to build correct software, with a strong focus on testing and program analysis. In particular, covered topics include:

  • Code documentation
  • Modularity and coupling (Design patterns)
  • Dynamic program analysis (Testing, fuzzing, concolic execution)
  • Static program analysis (Numerical abstract interpretation, pointer analysis, symbolic execution)
  • Formal modeling (Alloy)

Students apply the learned techniques to solve a group project in the area of program analysis.

Organization

Note that the modalities described below are subject to change throughout the semester.

Lectures

  • Lectures will be held online: they will be pre-recorded and published here in advance (credentials can be found here). We recommend watching these during regular lecture hours.
  • There will be no in-presence live streaming. In particular, the lecture hall (HG F 3) will not be used.
  • Each Wed at 13:40-14:00, the lecturers offer an online Q&A session (Zoom link ) on the topics of that week. Q&A sessions will not be recorded.

Exercises

  • Exercise sheets will be published here by Wednesday evening. Please solve the exercises before next week's exercise session and before looking at the solutions.
  • Exercise sessions start in the second week of the semester. There will be both online and physical exercise sessions, as listed below (students can freely chose which session to attend). We will discuss the solutions of the previous week's exercise sheet.
    • Group 1 (Mon 14-16): Physical in ML F 34
    • Group 2 (Mon 16-18): Online via Zoom
    • Group 3 (Thu 16-18): Online via Zoom (merged with group 4)
    • Groups 3 + 4 (Thu 16-18): Online via Zoom
  • Exercise sessions will not be recorded.

Moodle

  • For any additional questions regarding the lectures or exercises, we have prepared a Moodle forum.

To join the Zoom meetings, you must be logged in with a *.ethz.ch account, which you can create here.

Lectures

Use your NETHZ account to access the slides. Use these credentials to access the recordings.

DateContentSlidesRecordings
Feb 22Introduction PDF
Feb 23Documentation PDF
Mar 1Modularity PDF
Mar 2Functional Testing PDF
Mar 8Structural Testing PDF
Mar 9Guest (Veselin Raychev): DevOps PDF
Mar 15Analysis Introduction I PDF
Mar 16Analysis Introduction II PDF
Mar 22Analysis Math I PDF
Mar 23Analysis Math II PDF
Mar 29Project Introduction PDF
Mar 30Analysis Math III
Intervals I
PDF PDF
Apr 5Intervals II PDF
Apr 6Intervals III PDF
Apr 12Pointer Analysis PDF
Apr 13(no new content)    
Apr 18 - Apr 22: Easter break (no lectures or exercise sessions)    
Apr 26Applications I PDF
Apr 27Applications II PDF
May 3Rigorous Testing PDF
May 4Analysis Outlook (optional) (none)
May 10Guest (Jingxuan He): Fuzzing PDF
May 11Dynamic Race Detection PDF
May 17Alloy I PDF
May 18Alloy II PDF
May 24Alloy III PDF
May 25Guest (Andrei Dan): Alloy Memory PDF

Exercises

Use your NETHZ account to access the exercises.

No. Due DateContentExercisesSolutions
1 Feb 28 Documentation and Contracts PDF PDF updated
2 Mar 7 Modularity and Functional Testing PDF PDF PDF PDF
3 Mar 14 Structural Testing PDF PDF
4 Mar 21 First Steps with Abstract Interpretation PDF PDF
5 Mar 28 Mathematical Concepts PDF PDF
6 Apr 4 Approximation and Transformers PDF PDF
7 Apr 11 Interval Analysis PDF PDF
8 Apr 25 Pointer Analysis PDF PDF
9 May 2 Verifying Determinism PDF PDF
10 May 9 Symbolic Execution PDF PDF
11 May 16 Dynamic Race Detection PDF PDF
12 May 23 Static Alloy Models PDF PDF
13 May 30 Dynamic Alloy Models PDF PDF PDF PDF

Project

Details on the course project have been communicated on March 29 in the lecture. You can find instructions in your GitLab project repository.

Previous exams

Previous exams are available in the exam collection of the student association (VIS).