Automated Verification of Integer Overflow
Asankhaya Sharma

TL;DR
This paper introduces an automated method for verifying integer overflow in software, providing a new specification mechanism and a prototype tool that successfully identified 43 bugs in existing verified programs.
Contribution
It presents a novel specification mechanism for integer overflow and an automated verification procedure, along with a prototype tool tested on real-world code.
Findings
Identified 43 integer overflow bugs in verified programs
Developed a prototype overflow checker tool
Validated the approach on a 14k LOC benchmark
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Formal Methods in Verification · Software Reliability and Analysis Research
