O. Ponsini, C. Fédèle, and E. Kounalis (France)
Program Verification, Rewriting, Equational Semantics
This paper describes a system for automatically trans forming programs written in a simple imperative language (called C--), into a set of first-order equations. This means that a set of first-order equations used to represent a C-- program already has a precise mathematical meaning; moreover, the standard techniques for mechanizing equa tional reasoning can be used for verifying properties of pro grams. This work shows that simple imperative programs can be seen as fully formalized logical systems, within which theorems can be proved. The system itself is formu lated abstractly as a set of first-order rewrite rules. Then, it is proven to be terminating and confluent using the RRL system.
Important Links:
Go Back
