Overview

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

  • 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 generally be held in-person in HG F 3.
  • Recordings can generally be found here.

Exercises

  • Exercise sheets will be published here by Thursday 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): Physical in LFW C 5
      • Group 4 (Thu 16-18): Physical in ML H41.1 Merged with Group 3
  • 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.

DateContentSlides
Feb 22Introduction PDF
Feb 23Documentation PDF
Mar 01Modularity PDF
Mar 02Functional Testing PDF
Mar 08Guest Lecture -- DevOps PDF
Mar 09Structural Testing PDF
Mar 15Analysis Intro I PDF
Mar 16Analysis Intro II PDF
Mar 22Analysis Math I PDF
Mar 23Analysis Math II PDF
Mar 29Analysis Math III and Project Introduction PDF PDF
Mar 30Intervals I PDF
Apr 5Intervals II PDF
Apr 6Pointers I PDF
Apr 19Pointers II PDF
Apr 20Determinism I PDF
Apr 26Determinism II, Abstract Interpretation Outlook, Rigorous Testing I PDF PDF PDF PDF
Apr 27Project Q&A
May 03Rigorous Testing II PDF
May 04Guest Lecture: Fuzzing & Symbolic Execution PDF
May 11Alloy I PDF
May 17Alloy II PDF
May 24Alloy III PDF
May 25SAT and SMT PDF
May 31Guest Lecture: Alloy IV PDF
Jun 1Summary

Exercises

Use your NETHZ account to access the exercises.

No. Due DateContentExercisesSolutions
1 Feb 27 Documentation and Contracts PDF PDF updated
2 Mar 6 Modularity and Functional Testing PDF PDF updated PDF PDF updated
3 Mar 13 Structural Testing PDF PDF
4 Mar 20 First Steps with Abstract Interpretation PDF PDF
5 Mar 27 Mathematical Concepts of Abstract Interpretation PDF PDF
6 Apr 3 Approximation and Transformers PDF PDF
7 Apr 17 Interval Analysis PDF PDF
8 Apr 24 Pointer Analysis PDF PDF
9 May 3 Verifying Determinism PDF PDF
10 May 10 Symbolic Execution PDF PDF
11 May 17 Alloy I PDF PDF
13 May 24 Alloy II PDF PDF
12 May 31 Alloy III (updated 31.05.23, 01.06.23) PDF file updated PDF file updated

Project

Details on the course project will be communicated in a dedicated lecture.

Previous exams

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