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