A theoretical and practical study of low-level program verification. - K. L. J. Sylva (1984)