Towards verification of SubCprograms with side effects

As the interest for formal methods grows within industry, the need for convenient and automated tools grows too. SOSSub C is an attempt to help the development of certified programs. It allows formal reasoning about imperative programs by translating programs written in Sub C , a simple imperative language, into equations. Programs are then axioms of a logical system within which proofs can be carried out. In this paper, we describe how SOSSub C deals with side effects on lists and procedure parameters.