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