Patent ID: 9275236
Filing Date: 2016-03-01
CPC Classification: G06F

Claim Text:
1. A method for securing a first program, referenced hereinafter as a target program with a second program, referenced hereinafter as a target representative program, a third program, referenced hereinafter as a lemma program, and a fourth program, referenced hereinafter as a composition program, each program comprising constitutive elements, said constitutive elements comprising a finite number of program points and evolution rules associated with the program points and defining the passage from one program point to another program point, and each program comprising a definition of a set of properties each property being associated with one or more of the constitutive elements of the program, said method comprising: constructing the composition program by defining at least one relation between at least one constitutive element of the target representative program and at least one constitutive element of the lemma program, said relation being named a correspondence relation; and exploiting the correspondence relation for establishing a relation between one property of the first program and at least one property of the lemma or composition program, said relation being named a “sufficiency relation” and being such that it creates an oriented relationship between one local property of a program, and one or more local properties of the same or another program such that the proof of the latter properties proves the first local property, or propagate the proof of said property to at least one property of the target program.