Name
Abstract | ||
|---|---|---|
This paper describes a system for automatically transformi ng 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 a lready has a precise mathematical meaning; moreover, the standard techniques for mechanizin g equational reasoning can be used for verifying properties of programs. This work shows that s imple imperative programs can be seen as fully formalized logical systems, within which theo rems can be proved. The system itself is formulated abstractly as a set of first-order rewrite rules. |
Year | Venue | Keywords |
|---|---|---|
2002 | JFPLC | sémantique opérati onnelle et équationnelle keywords:program verification,operational and equation al semantics,mots-clés :vérification de programme,réécriture,rewriting |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
2 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Olivier Ponsini | 1 | 46 | 4.49 |
| Laboratoire I | 2 | 0 | 0.34 |
| Sophia Antipolis | 3 | 151 | 17.37 |