Constructing Trusted Code Base


These days it is possible to run a C compiler or an operating system that are designed and implemented so that they work correctly for sure. You can learn how to use techniques that led to these achievements in this course.

The page of the course in USOSweb is here (in Polish) or here (in English).


Joint grade that takes into account software project and exam in proportion 45% and 55% respectively.


  1. Introduction: risk analysis, applications, existing verified software lecture 1, lecture 2, lecture 12, lecture 13
  2. Programs extracted from proofs - logical basis lecture 3 and Coq sources, lecture 4 and more Coq sources
  3. Formalization of a procedure to be extracted (Coq) lecture 5 and more Coq sources
  4. Verification of specification-annotated programs - logical basis
    Why3 sources for lecture 6;
    lecture 7 and its examples and additional materials and yet more additional materials;
    lecture 8
  5. Program verification - an example (Why3) a bigger example for the lecture 9, lecture 10 (on TFTP)
  6. Certification and other tools lecture 14


  1. Work on removing complaints by splint in the TFTP implementation.
  2. The assignment to prove in Coq is here.
  3. Environment to start work with Frama-C/Why3 is here.

Final exam

There will be some at some point.

This course receives financial support from the Intel Corporation via the Intel Labs Security Curriculum Initiative.

Valid HTML 4.01! Valid CSS!