1. A method comprising: modeling an invariant based on a recorded value pointed to by a string variable within a computer-based software application during the execution of the computer-based software application, where the invariant represents at least one possible value pointed to by the string variable; recording the value pointed to by the string variable within the computer-based software application during the execution of the computer-based software application; executing the computer-based software application a plurality of times; performing the recording of the value pointed to by the string a plurality of times to record a plurality of values pointed to by the string variable, wherein the modeling of the invariant comprises modeling the invariant based on the plurality of values; performing a first static analysis of the computer-based software application using a theorem prover to determine whether the invariant is valid with respect to the computer-based software application; and seeding a second static analysis of the computer-based software application with the invariant if the invariant is valid with respect to the computer-based software application; wherein the recording, the modeling, the performing, and the seeding are implemented in at least one of: a) computer hardware, and b) computer software embodied in a non-transitory, computer-readable storage medium.