L4.sec implementation and formal verification

Gernot Heiser gernot at nicta.com.au
Sat Aug 26 05:12:28 CEST 2006

You may want to have a look at L4.verified.


>>>>> On Sat, 26 Aug 2006 04:05:11 +0200, William DUCK <guillaume.fortaine at wanadoo.fr> said:
WD>  Hello Misters,
WD> As you are microkernel experts, I am
WD>  asking your help.

WD>  I am attempting to build up a team.

WD>  I believe it's time for a full-fledge verified OS.

WD> If somebody is interested in functional programming and in formal methods to 
WD> help to implement the L4.sec kernel , he is welcome :)

WD> Here is an example of a protocol formalisation :

WD> network stack :
WD> http://www.cl.cam.ac.uk/~pes20/Netsem/

WD> If you want to contact me, my mail is guillaume_dot_fortaine_at_wanadoo_dot_fr

WD> I will set up a mailing-list, a web server, a wiki and an IRC

WD> Best Regards,

WD>                           Guillaume FORTAINE

More information about the l4-hackers mailing list