|
This course discusses some of the main ideas, techniques, and results in software verification. Three techniques that are widely used in practice will be discussed:
- Model checking, which provides efficient techniques for the exhaustive exploration of state-based models of programs and reactive systems.
- Static techniques for program analysis.
- Testing, which provides the counterpart to exhaustive techniques by defining dynamic analyses to detect programming mistakes and correct them.
The course includes weekly assignments that test understanding of the theoretical concepts that have been presented during the lecture, as well as the application of verification tools to illustrative examples. |
|
|
| This course builds on several of the previous courses in the Computer Science Bachelor's curriculum:
A basic knowledge is required of programming (course Imperative Programming, Object Orientation, and Functional Programming), logic (course Beweren & Bewijzen), automata theory (Talen & Automaten), concurrency and synchronization problems, and model checking (course on Operating Systems).
Also some of the concepts from the course Semantics & Correctness will be used during Software Verification course (it is fine, however, if you follow these two courses in parallel). |
|
| - Grading will be based on the exam (90%) and the weekly assignments (10%).
- To be admitted to the exam, you should have submitted serious attempts for 5 out of the 7 weekly assignments.
- For the Re-exam the same rules apply. However, there will be no second chance for the weekly assignments. |
|
|