Software Verificatie

Inleiding

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.

Leerdoelen

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, and theorem proving.

Onderwerpen

Model checking, theorem proving, static analysis, abstract interpretation.

Toetsvorm

  • Grading will be based on the exam and the practical assignments. The final grade is 0.6 E + 0.2 (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.

Vereiste voorkennis

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 and Object Orientation), 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).

Literatuur

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.


Deze cursus heeft ook een Engelstalige beschrijving.

Vakcode
NWI-IBC024
Studiepunten
3 ec
Periode
derde kwartaal

Docenten

Opgenomen in

  • Bachelor Informatica