Formal Verification of an O. S. Submodule. - N. S. Pendharkar; K. Gopinath (FSTTCS, 1998)