Automatic verification of possible software doubtful defects
Tang Yanwu · Journal of Tsinghua University(Science and Technology) · 2009
Manual verification of possible software defects is labor intensive and error prone.This paper presents an automatic verification method for possible software defects based on finite backtracking symbolic execution.The method first finds possible path fragments that may trigger defects,then collects the path conditions using symbolic execution to automatically verify the code.Tests of buffer overflow defects on the real code in OPENSSL are promising.