Using simplex method in verifying software safety

Abstract

In this paper we have discussed the application of the Simplex method in checking software safety - the application in automated detection of buffer overflows in C programs. This problem is important because buffer overflows are suitable targets for hackers' security attacks and sources of serious program misbehavior. We have also described our implementation, including a system for generating software correctness conditions and a Simplex based theorem prover that resolves these conditions.