Path: utzoo!attcan!uunet!jarthur!brutus.cs.uiuc.edu!uakari.primate.wisc.edu!uwm.edu!cs.utexas.edu!swrinde!ucsd!ucbvax!agate!darkstar!cis.ohio-state.edu
From: mandal@cis.ohio-state.edu (Manas Mandal)
Newsgroups: comp.os.research
Subject: Correctness of Operating Systems Implementations
Keywords: correctness, implementations, operating systems
Message-ID: <1130@darkstar.ucsc.edu>
Date: 7 Feb 90 21:29:18 GMT
Sender: usenet@darkstar.ucsc.edu
Lines: 10
Approved: comp-os-research@jupiter.ucsc.edu


I am interested in knowing about any work done in proving correctness
of operating systems implementations. Just like there are methods to
prove that a compiler correctly transforms a high-level program to a
machine program, I was wondering if anyone is working to show that the
implementation of an operating system correctly realizes its abstract
model.

Thanks,
Manas