Patent ID: 7020872

Claim:
A method for verifying transformation of a source code into a transformed code designed for an embedded system, said source and transformed codes being associated with virtual machines comprising: determining, for each of said source and transformed codes, a first common subset, constituting a single virtual machine that factors in the behavior of said source and transformed codes; determining, for each of said source and transformed codes, a second subset constituted by a plurality of auxiliary functions used by said single virtual machine, said auxiliary functions representing residual differences between said source and transformed codes and parameterizing the single virtual machine; associating said auxiliary functions in pairs, a first auxiliary function of each pair belonging to said second subset associated with said source code and a second auxiliary function of each pair belonging to said second subset associated with said transformed code; verifying a given correspondence property between said auxiliary functions of all of said pairs; and verifying that said transformation of the source code into a transformed code satisfies said given correspondence property.