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.
- 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 | |
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).