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 and will be recorded.
  • Recordings can be found here.

Exercises

  • Exercise sheets and corresponding solutions will be published here by Wednesday evening. Please solve the exercises before the next topics's exercise block and before looking at the solutions.
  • Exercise sessions start on Thursday in the first week of the semester (22.02). There will be identical sessions in Thursday-Monday blocks in person. The exercise sessions will consist of a discussion of the solutions of the previous problem sheet, a brief recap of the current week's topics, and a pre-discussion of the next problem sheet.
      • Groups 1 + 2 (Mon 14-16): Physical in IFW A 36
      • Groups 3 + 4 (Thur 16-18): Physical in LFW C 5
  • Exercise sessions will not be recorded.

Moodle

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

Lectures

Use your NETHZ account to access the slides.

DateContentSlides
Feb 21Introduction PDF
Feb 22Documentation PDF
Feb 28Modularity I PDF
Feb 29Modularity II, Testing I PDF PDF
Mar 6Testing II PDF
Mar 7Testing III PDF
Mar 13Analysis Intro I PDF
Mar 14Analysis Intro II PDF
Mar 20Analysis Math I PDF
Mar 21Analysis Math II PDF
Mar 27Project Introduction PDF
Mar 28Intervals I PDF
Apr 10Intervals II PDF
Apr 11Intervals III & Pointers I PDF PDF
Apr 17Pointers II & Determinism I PDF PDF
Apr 18Determinism II & Abstract Interpretation Outlook PDF PDF
Apr 24Rigorous Testing I PDF PDF
Apr 25Project Q&A & Rigorous Testing II PDF
May 2No Lecture
May 8Guest Lecture: Program analysis and Datalog solvers PDF
May 15Alloy I PDF
May 16Alloy II PDF
May 22Alloy III PDF
May 23SAT and SMT PDF
May 29Guest Lecture: Alloy IV PDF
May 30No Lecture

Exercises

Use your NETHZ account to access the exercises.

No. Due DateContentExercisesSolutions
1 Feb 29 Documentation and Contracts PDF PDF
2 Mar 7 Modularity and Functional Testing PDF PDF updated PDF PDF updated
3 Mar 14 Structural Testing PDF PDF updated
4 Mar 21 First Steps with Abstract Interpretation PDF PDF
5 Mar 28 Mathematical Concepts of Abstract Interpretation PDF PDF
6 Apr 11 Approximation and Transformers PDF PDF
7 Apr 18 Interval Analysis PDF PDF
8 Apr 25 Pointer Analysis PDF PDF
9 May 2 Verifying Determinism PDF PDF
10 May 8 Symbolic Execution PDF PDF
11 May 15 Alloy I & II PDF PDF PDF PDF
12 May 22 Alloy III PDF PDF

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).