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.
- 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.
| Date | Content | Slides | Recordings |
|---|---|---|---|
| Feb 22 | Introduction |
|
|
| Feb 23 | Documentation |
|
|
| Mar 1 | Modularity |
|
|
| Mar 2 | Functional Testing |
|
|
| Mar 8 | Structural Testing |
|
|
| Mar 9 | Guest (Veselin Raychev): DevOps |
|
|
| Mar 15 | Analysis Introduction I |
|
|
| Mar 16 | Analysis Introduction II |
|
|
| Mar 22 | Analysis Math I |
|
|
| Mar 23 | Analysis Math II |
|
|
| Mar 29 | Project Introduction |
|
|
| Mar 30 | Analysis Math III Intervals I |
|
|
| Apr 5 | Intervals II |
|
|
| Apr 6 | Intervals III |
|
|
| Apr 12 | Pointer Analysis |
|
|
| Apr 13 | (no new content) | ||
| Apr 18 - Apr 22: Easter break (no lectures or exercise sessions) | |||
| Apr 26 | Applications I |
|
|
| Apr 27 | Applications II |
|
|
| May 3 | Rigorous Testing |
|
|
| May 4 | Analysis Outlook (optional) | (none) |
|
| May 10 | Guest (Jingxuan He): Fuzzing |
|
|
| May 11 | Dynamic Race Detection |
|
|
| May 17 | Alloy I |
|
|
| May 18 | Alloy II |
|
|
| May 24 | Alloy III |
|
|
| May 25 | Guest (Andrei Dan): Alloy Memory |
|
|
Exercises
Use your NETHZ account to access the exercises.
| No. | Due Date | Content | Exercises | Solutions |
|---|---|---|---|---|
| 1 | Feb 28 | Documentation and Contracts |
|
updated
|
| 2 | Mar 7 | Modularity and Functional Testing |
|
|
| 3 | Mar 14 | Structural Testing |
|
|
| 4 | Mar 21 | First Steps with Abstract Interpretation |
|
|
| 5 | Mar 28 | Mathematical Concepts |
|
|
| 6 | Apr 4 | Approximation and Transformers |
|
|
| 7 | Apr 11 | Interval Analysis |
|
|
| 8 | Apr 25 | Pointer Analysis |
|
|
| 9 | May 2 | Verifying Determinism |
|
|
| 10 | May 9 | Symbolic Execution |
|
|
| 11 | May 16 | Dynamic Race Detection |
|
|
| 12 | May 23 | Static Alloy Models |
|
|
| 13 | May 30 | Dynamic Alloy Models |
|
|
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).