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
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.
- 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.
| Date | Content | Slides |
|---|---|---|
| Feb 22 | Introduction |
|
| Feb 23 | Documentation |
|
| Mar 01 | Modularity |
|
| Mar 02 | Functional Testing |
|
| Mar 08 | Guest Lecture -- DevOps |
|
| Mar 09 | Structural Testing |
|
| Mar 15 | Analysis Intro I |
|
| Mar 16 | Analysis Intro II |
|
| Mar 22 | Analysis Math I |
|
| Mar 23 | Analysis Math II |
|
| Mar 29 | Analysis Math III and Project Introduction |
|
| Mar 30 | Intervals I |
|
| Apr 5 | Intervals II |
|
| Apr 6 | Pointers I |
|
| Apr 19 | Pointers II |
|
| Apr 20 | Determinism I |
|
| Apr 26 | Determinism II, Abstract Interpretation Outlook, Rigorous Testing I |
|
| Apr 27 | Project Q&A | |
| May 03 | Rigorous Testing II |
|
| May 04 | Guest Lecture: Fuzzing & Symbolic Execution |
|
| May 11 | Alloy I |
|
May 17 | Alloy II |
|
| May 24 | Alloy III |
|
| May 25 | SAT and SMT |
|
| May 31 | Guest Lecture: Alloy IV |
|
| Jun 1 | Summary |
Exercises
Use your NETHZ account to access the exercises.
| No. | Due Date | Content | Exercises | Solutions |
|---|---|---|---|---|
| 1 | Feb 27 | Documentation and Contracts |
|
updated
|
| 2 | Mar 6 | Modularity and Functional Testing |
updated
|
updated
|
| 3 | Mar 13 | Structural Testing |
|
|
| 4 | Mar 20 | First Steps with Abstract Interpretation |
|
|
| 5 | Mar 27 | Mathematical Concepts of Abstract Interpretation |
|
|
| 6 | Apr 3 | Approximation and Transformers |
|
|
| 7 | Apr 17 | Interval Analysis |
|
|
| 8 | Apr 24 | Pointer Analysis |
|
|
| 9 | May 3 | Verifying Determinism |
|
|
| 10 | May 10 | Symbolic Execution |
|
|
| 11 | May 17 | Alloy I |
|
|
| 13 | May 24 | Alloy II |
|
|
| 12 | May 31 | Alloy III (updated 31.05.23, 01.06.23) |
updated
|
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).