SMT Solvers for Integer Overflows
Qixue Xiao, Yu Chen, Hui Fei Huang, Lanhan Qi · 2013
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 Boo lector, 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.