Determining correctness conditions for use in static analysis

Abstract

An embodiment comprising a method is associated with static analysis of a program, which detects violations of conditions of the program correctness specification. The method includes selectively encoding the program and adding one or more correctness conditions to the encoded program, wherein the added conditions comprise a set of assumptions that render the program correct with respect to one or more properties pertaining to detected violations. The set of assumptions are reported to a program user, together with a request to the user to verify the validity of each assumption of the set.

What is claimed is: 
     
         1 . A computer program product executable in a recordable storage medium for use with static analysis of a computer program, wherein the program has a related correctness specification and the static analysis detects violations of one or more conditions of the correctness specification, comprising:
 instructions for selectively encoding the program;   instructions for adding one or more correctness conditions to the encoded program, wherein the added conditions comprise a set of assumptions that render the program correct with respect to one or more properties pertaining to detected violations; and   instructions for reporting the set of assumptions to a program user, together with a request to the user to verify the validity of each assumption of the set.   
     
     
         2 . The computer program product of  claim 1 , wherein:
 responsive to a failure of the user to verify the validity of each assumption of the set of assumptions, the user is subsequently requested to verify the validity of one or more different assumptions.   
     
     
         3 . The computer program product of  claim 1 , wherein:
 the program is encoded as a first logical formula that is selectively processed to generate a second logical formula associated with the negation of at least the conditions of the correctness specification pertaining to the detected violations, and the correctness conditions are added to the second logical formula to produce a third logical formula associated with the set of assumptions.   
     
     
         4 . The computer program product of  claim 3 , wherein:
 the second logical formula is generated by conjoining the first logical formula with a formula that describes the negation of at least the conditions of the correctness specification pertaining to the detected violations.   
     
     
         5 . The computer program product of  claim 3 , wherein:
 responsive to the user confirming the validity of the assumption and added correctness conditions, the third logical formula is used for a further static analysis of the computer program, and violations detected thereby are reported to the user.   
     
     
         6 . The computer program product of  claim 3 , wherein:
 the third logical formula comprises a formula of propositional logic.   
     
     
         7 . The computer program product of  claim 6 , wherein:
 responsive to finding a satisfying assumption for the propositional logic formula, a subset of variables associated with the satisfying assumption are used to locate violations in the computer program.   
     
     
         8 . The computer program product of  claim 7 , wherein:
 a satisfiability solver is used to find a satisfying assumption.   
     
     
         9 . The computer program product of  claim 1 , wherein:
 said set of assumptions includes adding a specified element to the correctness specification of the computer program.   
     
     
         10 . The computer program product of  claim 1 , wherein:
 said set of assumptions includes making a specified fix to the code of the computer program.   
     
     
         11 . A computer system, for use with static analysis of a computer program, wherein the program has a related correctness specification and the static analysis detects violations of one or more conditions of the correctness specification, comprising:
 a bus;   a memory connected to the bus, wherein program code is stored on the memory; and   a processor unit connected to the bus, wherein the processor unit executes the program code to selectively encode the program; add one or more correctness conditions to the encoded program, wherein the added conditions comprise a set of assumptions that render the program correct with respect to one or more properties pertaining to detected violations; and report the set of assumptions to a program user, together with a request to the user to verify the validity of each assumption of the set.   
     
     
         12 . The system of  claim 11 , wherein:
 responsive to a failure of the user to verify the validity of each assumption of the set of assumptions, the user is subsequently requested to verify the validity of one or more different assumptions.   
     
     
         13 . The system of  claim 11 , wherein:
 the program is encoded as a first logical formula that is selectively processed to generate a second logical formula associated with the negation of at least the conditions of the correctness specification pertaining to the detected violations, and the correctness conditions are added to the second logical formula to produce a third logical formula associated with the set of assumptions.   
     
     
         14 . The system of  claim 13 , wherein:
 the second logical formula is generated by conjoining the first logical formula with a formula that describes the negation of at least the conditions of the correctness specification pertaining to the detected violations.   
     
     
         15 . The system of  claim 13 , wherein:
 responsive to the user verifying the validity of each assumption of the set of assumptions, the third logical formula is used for a further static analysis of the computer program, and violations detected thereby are reported to the user.   
     
     
         16 . The system of  claim 13 , wherein:
 the third logical formula comprises a formula of propositional logic.   
     
     
         17 . The system of  claim 16 , wherein:
 responsive to finding a satisfying assumption for the propositional logic formula, a subset of variables associated with the satisfying assumption are used to locate violations in the computer program.   
     
     
         18 . The system of  claim 17 , wherein:
 a satisfiability solver is used to find a satisfying assumption.   
     
     
         19 . The system of  claim 11 , wherein:
 said set of assumptions includes adding a specified element to the correctness specification of the computer program.   
     
     
         20 . The method of  claim 11 , wherein:
 said set of assumptions includes making a specified fix to the code of the computer program.