# US 9,436,582 B1 · Calculating an immediate parent assertion statement for program verification > Agents: this data is available as JSON from the patentgrep API and MCP server — see https://patentgrep.com/llms.txt - Number: US 9,436,582 B1 - Document ID: US9436582B1 - Status: Granted - Kind: B1 - Application number: 14/944,330 - Filed: 2015-11-18 - Granted: 2016-09-06 - Earliest claimed: 2015-11-18 - Assignees: International Business Machines Corporation - Applicants: International Business Machines Corporation - Inventors: Viresh Paruthi; Mitra Purandare - Web page: https://patentgrep.com/patent/US9436582B1 ## CPC - G06F 11/3608: {using formal methods, e.g. model checking, abstract interpretation (theorem proving G06N5/013)} - G06F: ELECTRIC DIGITAL DATA PROCESSING (computer systems based on specific computational models G06N) ## Abstract Embodiments include dividing source code for an application into multiple program fragments by generating a control flow graph for the multiple program fragments. The control flow graph represents a graph structure with nodes representing the multiple program fragments and edges representing an execution order of the program fragments. Aspects include searching for a chosen assertion statement within a program fragment, wherein the chosen assertion statement must be satisfied for correct execution of the chosen program fragment. Aspects also include 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 immediate parent program fragment using the chosen assertion logic statement. The immediate parent assertion statement is an over-approximate pre-condition of the chosen program fragment. The computation of the over-approximate pre-condition is performed by computing a precondition that satisfies the chosen assertion statement and the particular-precondition. ## Claims ### Claim 1 A computer program product, the computer program product comprising a computer readable storage medium having program instructions embodied therewith, wherein the computer readable storage medium is not a transitory signal per se, the program instructions being executable by a processor to cause the processor to perform a method comprising: dividing source code for an application into multiple program fragments; generating 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; 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 immediate parent program fragment using the chosen program fragment and 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. ### Claim 2 (depends on 1) The computer program product of claim 1, wherein the program instructions further cause the processor to perform the method step comprising determining if the immediate parent assertion statement is satisfied within the immediate parent program fragment. ### Claim 3 (depends on 1) The computer program product of claim 1, wherein the program instructions further cause the processor to perform the method step comprising determining if the immediate parent assertion statement is satisfied within the immediate parent program fragment using a SAT or SMT solver. ### Claim 4 (depends on 2) The computer program product of claim 2, wherein the control flow graph has a root node, wherein the program instructions further cause the processor to perform the method steps comprising repeated identification of the immediate parent program fragment and calculating the immediate parent assertion statement, and determining if the immediate parent assertion statement is satisfied within the immediate parent program fragment until either the immediate parent assertion statement is not satisfiable or the root node of the control flow graph is reached. ### Claim 5 (depends on 2) The computer program product of claim 2, wherein the program instructions further cause the processor to perform the method step comprising outputting data identifying the immediate parent program fragment if the immediate parent assertion statement fails to be satisfied in the immediate parent program fragment. ### Claim 6 (depends on 5) The computer program product of claim 5, wherein the computer system comprises a graphical user interface, wherein the program instructions further cause the processor to perform the method step comprising displaying the data identifying the immediate parent program fragment on the graphical user interface. ### Claim 7 (depends on 1) The computer program product of claim 1, wherein calculation of the immediate parent assertion statement for the immediate parent program fragment using the chosen assertion statement is at least partially performed by: eliminating or unwinding loops and function calls within the chosen program fragment; and converting the chosen program fragment into static single assignment form; computing an over-approximate pre-condition for the chosen assertion statement within the chosen program fragment that has been converted into single static assignment form, wherein the over-approximate pre-condition is the immediate parent assertion statement. ### Claim 8 (depends on 1) The computer program product of claim 1, wherein over-approximating the particular pre-condition using interpolation is at least partially performed by: converting the chosen program fragment and its chosen assertion into a logical formula using static single assignment form; solving the logical formula returning a satisfying assignment, wherein a satisfying assignment is a partial pre-condition restricting the partial pre-condition to input variables of the chosen program fragment, converting the chosen program fragment and negation of the chosen assertion statement into a logical formula corresponding to error reachability using static single assignment form; and solving a conjunction of the restricted partial pre-condition and the logical formula corresponding to error reachability resulting in a proof of unsatisfiablility, and computing the over approximate pre-condition using the proof of unsatisfiablility for interpolation. ### Claim 9 (depends on 8) The computer program product of claim 8, wherein over-approximating the particular pre-condition using interpolation is performed repeatedly to over-approximate all possible partial pre-conditions of solving the logical formula corresponding to static single assignment form of the chosen program fragment and its chosen assertion. ### Claim 10 (depends on 8) The computer program product of claim 8, wherein over-approximating the particular pre-condition using interpolation is performed repeatedly for all partial pre-conditions of solving the logical formula corresponding to static single assignment form of the chosen program fragment and its chosen assertion to over-approximate a partial pre-condition until the over-approximation converges to a fixed point, wherein the fixed point is the over approximate pre-condition. ### Claim 11 (depends on 1) The computer program product of claim 1, wherein the control flow graph is generated by tracing program flow and function calls in the source code. ### Claim 12 (depends on 1) The computer program product of claim 1, wherein the division of the source code into multiple program fragments is performed by any one of the following: identifying transitions between programming languages, identifying sub routine calls, identifying function calls, identifying conditional blocks, identifying execution loops, identifying code libraries of the source code, identifying subroutines in the source code, breaking sections of the source code more than a predetermined number of lines into program fragments, breaking sections of the source which contain more than a predetermined number of program statements into program fragments, and combinations thereof. ### Claim 13 (depends on 1) The computer program product of claim 1, wherein the control flow graph is a call tree or a call graph. ### Claim 14 (depends on 1) The computer program product of claim 1, wherein the program instructions further cause the processor to perform the method step comprising deriving the chosen assertion statement from any one of the following: an argument to an assert macro, an illegal argument exception, a program statement to generate error code, a statement for generating error handing code, and one or more program statements for invoking an error handler. ### Claim 15 (depends on 1) The computer program product of claim 1, wherein the source code comprises multiple libraries. ### Claim 16 (depends on 1) The computer program product of claim 1, wherein the source code is written in multiple computer programming languages. ### Claim 17 (depends on 1) The computer program product of claim 1, wherein the program instructions at least partially implement an integrated development environment. ### Claim 18 (depends on 1) The computer program product of claim 1, wherein the program instructions at least partially implement a compiler. ### Claim 19 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. ### Claim 20 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.