Calculating an immediate parent assertion statement for program verification

A computer system comprising:

• a memory containing machine executable instructions and source code for an application;
• and
• a processor for executing the machine executable instructions, wherein execution of the machine executable instructions causes the processor to:
• divide the source code into multiple program fragments;
• generate a control flow graph for the multiple program fragments, wherein the control flow graph represents a graph structure with nodes representing the multiple program fragments and edges representing an execution order of the multiple program fragments;
• search for a chosen assertion statement within a chosen program fragment, wherein the chosen program fragment is selected from the multiple program fragments, wherein the chosen assertion statement must be satisfied for correct execution of the chosen program fragment;
• identify an immediate parent program fragment for the chosen program fragment using the control flow graph;
• and
• calculate an immediate parent assertion statement for the calling program fragment using the chosen assertion statement, wherein if the immediate parent assertion statement is satisfied in the immediate parent program fragment then the chosen assertion statement is satisfied in the chosen program fragment, wherein the immediate parent assertion statement is an over-approximate pre-condition of the chosen program fragment, wherein the computation of the over-approximate pre-condition is performed by:
• computing a particular precondition that satisfies the chosen assertion statement with a solver and over-approximating the particular-precondition using interpolation.

A computer implemented method, wherein the method comprises:

• dividing source code of an application into multiple program fragments;
• generating an control flow graph for the multiple program fragments, wherein the control flow graph represents a graph structure with nodes representing the multiple program fragments and edges representing an execution order of the multiple program fragments;
• searching for a chosen assertion statement within a chosen program fragment, wherein the chosen program fragment is selected from the multiple program fragments, wherein the chosen assertion statement must be satisfied for correct execution of the chosen program fragment;
• identifying an immediate parent program fragment for the chosen program fragment using the control flow graph;
• and
• calculating an immediate parent assertion statement for the calling program fragment using the chosen assertion statement, wherein if the immediate parent assertion statement is satisfied in the immediate parent program fragment then the chosen assertion statement is satisfied in the chosen program fragment, wherein the immediate parent assertion statement is an over-approximate pre-condition of the chosen program fragment, wherein the computation of the over-approximate pre-condition is performed by:
• computing a particular precondition that satisfies the chosen assertion statement with a solver and over-approximating the particular-precondition using interpolation.