A method for buffer overflow detection involves obtaining a program code configured to access memory locations in a loop using a buffer index variable, obtaining an assertion template configured to capture a dependency between the buffer index variable and a loop index variable of the loop in the program code, generating an assertion using the assertion template, verifying that the assertion holds using a k-induction; and determining whether a buffer overflow exists using the assertion.