This course builds on several of the previous courses in the Computer Science bachelor 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).
After successfully taking this course, students will have a theoretical and practical understanding of the principles behind fundamental software verification techniques, including model checking, static analysis, in particular type systems, and theorem proving.
The idea of software verification has been around for decades, but only recently have the techniques become mature enough to be applicable in practice. Key to this success has been (a) combination of previously developed techniques, and (b) automation.
This course embraces this diversity of approaches, by surveying some of the main ideas, techniques, and results in software verification. These include in particular:
- Model checking, which provides efficient techniques for the exhaustive exploration of state-based models of programs and reactive systems.
- Static techniques for program analysis.
- Theorem proving, which, in principle, enables the verification of any program.
To demonstrate some of the techniques in practice, the course will offer two practical projects requiring the application of verification tools to illustrative examples.
Model checking, theorem proving, typing, abstract interpretation (tentative).
- Grading will be based on the exam and the practical assignments. The final grade is 0.7 E + 0.15 (P1 + P2), where E is the result of the exam, and P1 and P2 are the results of the two practical assignments.
- The grade for the exam must be at least 5: if the grade for the exam is below 5 then the final grade of the course equals the grade for the exam.
- To be admitted to the exam, you should have submitted serious attempts for the two practical assignments, and for 75% of the weekly assignments.
- For the Re-exam the same rules apply. However, there will no second chance for the practical and weekly assignments.
The course material consists of hand-outs and lecture slides. These will be made available electronically via Blackboard. The theory discussed in the first three lectures is presented in the textbook Principles of model checking,Christel Baier and Joost-Pieter Katoen, Cambridge, Mass: MIT Press, 2008.