×

zbMATH — the first resource for mathematics

Using simplex method in verifying software safety. (English) Zbl 1274.90227
Summary: We discuss 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 also describe our implementation, including a system for generating software correctness conditions and a Simplex based theorem prover that resolves these conditions.
MSC:
90C05 Linear programming
90C90 Applications of mathematical programming
Software:
Flawfinder; SMT-LIB
PDF BibTeX XML Cite
Full Text: DOI