Program Verification by Calculating Relations

J. Carette, R. Janicki, and Y. Zhai (Canada)

Keywords

Modelling, Proving Program Correct ness, Symbolic Computation, Recurrence Relations

Abstract

We show how properties of an interesting class of imperative programs can be verifed by means of relational modelling and symbolic computation.

Important Links:



Go Back