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.
- Note: On Thu 27th of Feb, the lecture will take place in HG G 3!
- Recordings can be found here.
- However, we cannot guarantee that the recordings will capture all content and activity presented in the lecture, therefore we recommend attending the lectures in person.
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 19 | Introduction |
|
| Feb 20 | Documentation |
|
| Feb 26 | Modularity I |
|
| Feb 27 | Modularity II, Testing I (Change: the lecture will be in HG G 3) |
|
| Mar 5 | Testing II |
|
| Mar 6 | Testing III |
|
| Mar 12 | Analysis Intro I |
|
| Mar 13 | Analysis Intro II |
|
| Mar 19 | Analysis Math I |
|
| Mar 20 | Analysis Math II |
|
| Mar 26 | Project Introduction |
|
| Mar 27 | Intervals I |
|
| Apr 2 | Intervals II | |
| Apr 3 | Intervals III & Pointers I | |
| Apr 9 | Pointers II & Determinism I | |
| Apr 10 | Determinism II & Abstract Interpretation Outlook | |
| Apr 16 | Rigorous Testing I | |
| Apr 17 | Project Q&A | |
| Apr 30 | Rigorous Testing II | |
| May 1 | No lecture | |
| May 7 | Guest Lecture: Program analysis and Datalog solvers | |
| May 8 | Alloy I | |
| May 14 | Alloy II | |
| May 15 | Alloy III | |
| May 21 | SAT and SMT | |
| May 22 | Guest Lecture: Alloy IV | |
| May 28 | Summary |
Exercises
Use your NETHZ account to access the exercises.
| No. | Due Date | Content | Exercises | Solutions |
|---|---|---|---|---|
| 1 | Feb 27 | Documentation and Contracts |
|
|
| 2 | Mar 6 | Modularity and Functional Testing |
|
|
| 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 10 | Interval Analysis | ||
| 8 | Apr 17 | Pointer Analysis | ||
| 9 | May 5 | Verifying Determinism | 10 | May 8 | Symbolic Execution | 11 | May 15 | Alloy I | 12 | May 22 | Alloy II | 13 | May 29 | 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).