Patent ID: 8296735

Claim:
A computer method for the inter-procedural checking of source code, comprising: receiving source code comprising a list of functions; expressing a required inter-procedural check as a formula expressed in computational tree logic (CTL) syntax; decomposing the computational tree logic (CTL) syntax of the inter-procedural check into sub-formulae; automatically mapping the functions of the source code to respective sub-structures of an associated recursive Kripke structure, wherein the sub-structures call other substructures, and wherein each sub-structure comprises the following states: an entry location having internal guarantees, other locations representing code statements having respective internal guarantees, boxes that model calls to other functions, having respective internal assumptions and external guarantees, and an exit location having internal guarantees and external assumptions; wherein there are transitions between adjacent locations and boxes that map a value from an precursor location or box to a successor location or box; generating a summary for each substructure capable of being represented as a table wherein each row represents a location, box or the external assumptions of the substructure, and wherein each row comprises three values that respectively represent: whether the summary is an assumption for a box, a guarantee for a location or external assumptions, whether the current sub-formula is true, false or undetermined at that state when a first external assumption of that substructure is assumed to be false, and whether the current sub-formula is true, false or undetermined at that state when the other external assumption of that substructure is assumed to be true; then, starting with the simplest sub-formula, refining the summaries by: (i) applying computational tree logic (CTL) model checking to each sub-structure to check whether the each guarantee is true, false or undetermined for each external assumption and updating the corresponding values of the summary accordingly, then (ii) checking whether the internal assumptions of each box are consistent with the first internal guarantees of the callee sub-structure, and whether the external assumptions are consistent with the external guarantees of the caller sub-structure and updating the corresponding values of the summary accordingly, then, (iii) iteratively repeating steps (i) and (ii) until no further refinement of the sub-formula is possible; then iteratively repeating steps (i), (ii) and (iii) for each sub-formula in increasing complexity, until no further refining is possible for the most complex sub-formula, and therefore the entire formula.