1. A computer implemented method for analysing a program based on source code, the source code comprising a call to a function associated with a function implementation, the method comprising: determining, based on a summary that over-approximates the function, an assignment of an input variable and an output variable of the call to the function such that the assignment allows the program to reach a predefined state; determining, based on the implementation of the function whether the assignment of the input variable results in the assignment of the output variable; upon determining that the assignment of the input variable does not result in the assignment of the output variable, determining a narrowed summary for the function such that the narrowed summary over-approximates the function and excludes the assignment of the input variable and the output variable; and storing the narrowed summary associated with the function on a datastore.