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

Lectures

  • Lectures will be pre-recorded and published here in advance (credentials can be found here). We recommend watching these during regular lecture hours.
  • Each Wednesday at 11:40-12:00, Prof. Martin Vechev offers a virtual Q&A session (Zoom link ) on the topics of that week.
  • For additional questions, we have prepared a Moodle forum.

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 are conducted virtually and start in the second week of the semester. We will discuss the solutions of the previous week's exercise sheet. Please register for an exercise group via MyStudies.
  • For additional questions, 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.

Communication

All communication (including special announcements) will be sent out by e-mail. For written questions, please use the Moodle forum whenever possible. In exceptional cases, you can contact the head TA.

Lectures

Use your NETHZ account to access the slides. The credentials to access the recordings can be found here.

DateContentSlidesRecordings
Feb 23Introduction PDF
Feb 24Documentation PDF
Mar 2Modularity PDF
Mar 3Functional Testing PDF
Mar 9Structural Testing PDF
Mar 10Guest Lecture: Veselin Raychev PDF
Mar 16Analysis Introduction I PDF
Mar 17Analysis Introduction II
Mar 23Analysis Math I PDF
Mar 24Analysis Math II PDF
Mar 30Project Introduction PDF
Mar 31(No lecture)    
Apr 2 - Apr 11: Easter break (no lectures or exercise sessions)    
Apr 13Intervals I PDF
Apr 14Intervals II PDF
Apr 20Pointer Analysis I PDF
Apr 21Pointer Analysis II PDF
Apr 27Application I PDF
Apr 28Application II PDF
May 4Symbolic Execution PDF
May 5Concolic Execution PDF
May 11Guest Lecture: Jingxuan He PDF
May 12Dynamic Race Detection PDF
May 18Alloy I PDF
May 19Alloy II PDF
May 25Alloy III PDF
May 26Guest Lecture: Andrei Dan PDF
Jun 2Summary (no slides)

Exercises

Use your NETHZ account to access the exercises.

No. Due DateContentExercisesSolutions
1 Mar 1 Documentation and Contracts PDF PDF
2 Mar 8 Modularity and Functional Testing PDF PDF PDF PDF
3 Mar 15 Structural Testing PDF PDF
4 Mar 22 First Steps with Abstract Interpretation PDF PDF
5 Mar 29 Mathematical Concepts PDF PDF
6 Apr 19 Interval Analysis PDF PDF
7 Apr 26 Widening and Pointer Analysis PDF PDF
8 May 3 Verifying Determinism PDF PDF
9 May 10 Symbolic Execution PDF PDF
10 May 17 Dynamic Race Detection PDF PDF
11 May 24 Static Alloy Models PDF PDF
12 May 31 Dynamic Alloy Models PDF PDF PDF PDF

Project

The project will be conducted in groups of 2-3 students. We will send out a link for group registration on March 15. Groups must be registered by March 23. Use Moodle if you cannot find a team.

The project webpage is here.

Previous exams

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