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