Automated Verification of Integer Overflow
Programming Languages
2019-09-23 v1
Abstract
Integer overflow accounts for one of the major source of bugs in software. Verification systems typically assume a well defined underlying semantics for various integer operations and do not explicitly check for integer overflow in programs. In this paper we present a specification mechanism for expressing integer overflow. We develop an automated procedure for integer overflow checking during program verification. We have implemented a prototype integer overflow checker and tested it on a benchmark consisting of already verified programs (over 14k LOC). We have found 43 bugs in these programs due to integer overflow.
Cite
@article{arxiv.1909.09324,
title = {Automated Verification of Integer Overflow},
author = {Asankhaya Sharma},
journal= {arXiv preprint arXiv:1909.09324},
year = {2019}
}