As long as requirements to computer designs are formulated in an
ambiguous human language and as long as these designs are implemented by
humans not insured against possible carelessness and
misunderstandings, computer systems will contains errors. For the time
being, the only way to guarantee absence of errors in a computer
system is to exploit rigorous formal methods of mathematics for
specifying system's intended behavior and proving that the actual
system's implementation meets the desired behavior.
In the
seminar, we will consider articles describing how logic and
mathematics could be applied for precise specification and subsequent
verification of selected computer systems, e.g., processors, compilers,
and microkernels. In this semester, the focus of the considered
articles is on policy languages for expressing system requirements.
Participants of the seminar can use an opportunity to apply the studied techniques in the lab course "Formal Specification and Verification in Isabelle/HOL" that will take place in the same semester. However, the seminar and the lab course can also be taken individually.
- Dozent*in: Tobias Hamann