Patent attributes
Methods, systems, and apparatus, including computer programs encoded on a computer storage medium, for receiving source code and an indication that a portion of the source code is insecure. Receiving an annotation to the source code that identifies the indication as being a false positive indication. The annotation includes a logical statement showing that the portion of the source code is not insecure, where the logical statement can be executed by a processor to prove that the portion of the source code is not insecure. Processing the annotation to determine whether the logical statement proves that the portion of the source code is not insecure. In response to determining that the logical statement proves that the portion of the source code is not insecure, retaining the annotation in the source code, and removing the indication that the portion of the source code is insecure.