DETERMINING CORRECTNESS CONDITIONS FOR USE IN STATIC ANALYSIS

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.