Path: utzoo!utgpu!jarvis.csri.toronto.edu!clyde.concordia.ca!mcgill-vision!bloom-beacon!mintaka!yale!cs.utexas.edu!swrinde!ucsd!ucsdhub!hp-sdd!ncr-sd!ncrcae!hubcap!Manas
From: mandal@cis.ohio-state.edu (Manas Mandal)
Newsgroups: comp.parallel
Subject: Correctness of Operating Systems Implementations
Message-ID: <7915@hubcap.clemson.edu>
Date: 8 Feb 90 13:35:25 GMT
Sender: fpst@hubcap.clemson.edu
Lines: 13
Approved: parallel@hubcap.clemson.edu


Keywords: correctness, implementations, operating systems


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