Correct-Program Technology/Extensibility of Verifiers. Two Papers on Program Verification. by Martin Davis and J. T. Schwartz