An experiment in automatic verification of programs. - Gerald M. Weinberg; G. L. Gressett (Commun. ACM, 1963)