Software model checking has recently been successful in discovering bugs in production software. Most tools have targeted heap related programming mistakes and control-heavy programs. However, real-time and embedded controllers implemented in software are susceptible to computational numeric instabilities. We target verification of numerical programs that use floating-point types, to detect loss of numerical precision incurred in such programs. Techniques based on abstract interpretation have been used in the past for such analysis. We use bounded model checking (BMC) based on Satisfiability Modulo Theory (SMT) solvers, which work on a mixed integer-real model that we generate for programs with floating points. We have implemented these techniques in our software verification platform. We report experimental results on benchmark examples to study the effectiveness of model checking on such problems, and the effect of various model simplifications on the performance of model checking.
展开▼
