[IEEE 2015 International Conference on Computer Application Technologies (CCATS) - Matsue, Japan (2015.8.31-2015.9.2)] 2015 International Conference on Computer Application Technologies - Array Bounds Model Checking in C Code Based on Predicate Abstraction