1. 1

Abstract: “In the first part of this thesis, we present a case study on successfully verifying the Linux USB BP keyboard driver. Our verification approach is (a) sound, (b) takes into account dynamic memory allocation, complex API rules and concurrency, and (c) is applied on a real kernel driver which was not written with verification in mind. We employ VeriFast, a software verifier based on separation logic. Besides showing that it is possible to verify this device driver, we identify the parts where the verification went smoothly and the parts where the verification approach requires further research to be carried out.

In the second part of this thesis, we present a program verification approach that uses an input/output style of reasoning. It can be applied both to programs that perform input/output, and programs that do not but instead manipulate memory. The approach is sound, modular, compositional (I/O actions can be defined on top of other actions) and supports concurrency. It uses Petri nets and separation logic. We have implemented the approach, both for programs that do and do not perform I/O, in the VeriFast verifier and sketched how it can be implemented in the Iris framework for programs that perform I/O.”


  2. 1

    One reason I kept this is the section on I/O verification. Most verifications mention they don’t include I/O. That’s usually a small component, too, that can be verified in isolation if it’s designed right. So, I started looking for more work on that so people could use one set of techniques on computation, another on I/O, and then integrate. Also, petri nets and separation logic have long history with a number of tools/projects to support anyone building on them.