Cousot, P.; Cousot, R. “A la Burstall” intermittent assertions induction principles for proving inevitability properties of programs. (English) Zbl 0788.68094 Theor. Comput. Sci. 120, No. 1, 123-155 (1993). Reviewer: D.Tătar (Cluj) MSC: 68Q60 PDFBibTeX XMLCite \textit{P. Cousot} and \textit{R. Cousot}, Theor. Comput. Sci. 120, No. 1, 123--155 (1993; Zbl 0788.68094) Full Text: DOI
Makowsky, J. A.; Sain, I. Weak second order characterizations of various program verification systems. (English) Zbl 0678.68008 Theor. Comput. Sci. 66, No. 3, 299-321 (1989). Reviewer: R.Horsch MSC: 68Q60 03B70 03B60 PDFBibTeX XMLCite \textit{J. A. Makowsky} and \textit{I. Sain}, Theor. Comput. Sci. 66, No. 3, 299--321 (1989; Zbl 0678.68008) Full Text: DOI