The University of New South Wales

Acknowledgements

We would like to acknowledge the help and support that we received from our research partners and collaborators during this project.

In particular, we thank the development team of the Isabelle theorem prover for their help and support. Isabelle is the main verification tool used in this project and without its maturity success would not have been possible.

We thank the folks at Galois Inc who have worked with us to develop an open source proof library and theory for fixed-size machine words (e.g. 32 bit integers).

We also would like to acknowledge the contribution of our friendly competition, the German Verisoft project with whom we share some verification technology. In particular we would like to thank Norbert Schirmer whose verification framework for imperative programs we instantiate to the C language.

On the kernel side, the OS hackers at Open Kernel Labs have kept us on track and in connection with real-world customer requirements.

Finally, we thank (and you don't see that often in a research institution) the NICTA executive team who saw through our strange formulas, believed in the project and supported it from the beginning.

Dramatis Personae (aka The Team)

The L4.verified team over time included the following persons (in alphabetical order).