Patent ID: 7827534

Claim:
A method for determining the operational characteristics of a program, comprising a verification procedure comprising the following steps: a first step comprising: expressing the operational characteristics of the program as functions dealing with occurrences or sequences of occurrences of events occurring during executions of the program, said events being able to deal with particular operations, particular values of data, at particular program points and in particular states of the program; determining a level of precision with which these characteristics must be determined; determining a set of particular contexts of execution in which the program will always be executed; and determining operational specificities of a set of platforms on which the program will be executed; a second step of estimation, by program analysis, and in consideration of said level of precision, of said set of particular contexts of execution and of said operational specificities of platforms, of information relating to a structure of the program, execution paths of the program and to values of data, at various points of the execution paths and under different execution conditions, of states of the program and data handled by the program; and a third step for determining said operational characteristics, by means of the information extracted by said program analysis, by computation of said functions on the occurrences or particular sequences of occurrences of particular operations, dealing with particular values, at particular points of the program, in particular states of the program, for the set of execution paths determined by analysis.