[net.math] Formal Proofs of Operating System

albert@oliven.UUCP (LuigiAlberto Piodisavoia) (02/07/85)

I have recently heard of a paper which described a methodoloy for
providing a 'mathematical' proof of the correctness of an
operating system, unfortunately my source did not have more
information about this paper than the brief abstract I have just
typed.

I would appreciate any information regarding formal treatments of
operating systems, compilers etc.

I will post a summary of all work on the net.



	Alberto Savoia @ Olivetti Advanced Technology Center