SOS C- : A SYSTEM FOR INTERPRETINGOPERATIONAL SEMANTICS OF C- PROGRAMS
Olivier Ponsini, Carine Fédèle, Emmanuel Kounalis · 2002
This paper describes a system for automatically transforming 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