Stanford Pascal Verifier User Manual
David C. Luckham, Steven M. German, F. W. von Henke, Richard Alan Karp, Philip Milne · 1979
The Stanford PASCAL verifier is an interactive program verification system. It automates much of the work necessary to analyze a program for consistency with its documentation, and to give a rigorous mathematical proof of such consistency or to pin-point areas of inconsistency. It has been shown to have applications as an aid to programming, and to have potential for development as a new and useful tool in the production of reliable software.