SMT Solvers for Integer Overflows

SMT solver which is an automated program analysis technique is increasingly used by Vulnerability discovering platforms, especially in the integer security problems checking. An integer vulnerability discovering platform is mostly decided by the SMT solver. We have analyzed integer security problems and several SMT solvers, such as Boolector, Z3, STP and so on. We evaluated the ability of the SMT solvers in integer overflows checking from the view of vulnerability discovering. We also developed a set of APIs to check the integer overflows based on STP.