Page 1 of 1

Full fledge verified OS

Posted: Wed Aug 23, 2006 8:43 pm
by ziteribo
Hello Misters,

As you are interested in OS design, I am
asking your help.

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

http://www.ertos.nicta.com.au/publicati ... _KH_05.pdf

I am attempting to build a team.

*OS-design :

http://www.ertos.nicta.com.au/publicati ... lie_06.pdf ( for
transition )

http://www.marcus-brinkmann.org/hurd-ng.pdf

http://www.eecg.toronto.edu/~tornado/ ( scalability / hot swapping )

*kernel :

http://os.inf.tu-dresden.de/L4/L4.Sec/

http://www.doclsf.de/papers/vstte06.pdf ... 0kernel%22

*network stack :

http://www.cl.cam.ac.uk/~pes20/Netsem/

*programming :

http://fling-l.seas.upenn.edu/~plclub/c ... _Challenge

http://www.informatik.uni-bonn.de/~loeh/GFP.html

http://maude.cs.uiuc.edu/tools/scc/

*proving environment :

http://isabelle.in.tum.de/

http://www.cl.cam.ac.uk/Research/HVG/HOL/

*compiler :

http://pauillac.inria.fr/~xleroy/compcert-backend/

http://www.score.is.tsukuba.ac.jp/~okuma/vc/

Any suggestions ?

Thank you for your answer,

If you want to contact me, my mail is guillaume_dot_fortaine_at_wanadoo_dot_fr

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

Best Regards,

Guillaume FORTAINE

Posted: Fri Sep 01, 2006 8:00 pm
by earlz
could you please give a summary of all this, I dislike reading 30+ pages...