University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Verifying an Operating System Kernel

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Verifying an Operating System Kernel

Download to your calendar using vCal

If you have a question about this talk, please contact Thomas Tuerk .

Room changed

I will describe an ongoing project to verify a version of the L4 microkernel. I will describe some of the important logical problems, but also cover the pragmatics of marrying OS design and development (done by OS hackers) with the verification of the design and code (done by Isabelle users).

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Seminar Rooms 3 & 4, Churchill College Average on Sundays: 7478.1744186 kWh MR19 (note venue change!)

Other talks

Mergers all the way down: simulating the origin of globular clusters in a galactic context Defining and detecting discrimination: a new way forward title abstract tbc Spectral theory for Dirac operators with singular potentials TBC Loke CTR Seminar Series - Vincent Pasque
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity