TY - GEN
T1 - Numerical stability analysis of floating-point computations using software model checking
AU - Ivančić, Franjo
AU - Ganai, Malay K.
AU - Sankaranarayanan, Sriram
AU - Gupta, Aarti
PY - 2010
Y1 - 2010
N2 - Software model checking has recently been successful in discovering bugs in production software. Most tools have targeted heap related programming mistakes and controlheavy 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.
AB - Software model checking has recently been successful in discovering bugs in production software. Most tools have targeted heap related programming mistakes and controlheavy 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.
UR - http://www.scopus.com/inward/record.url?scp=77957796073&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=77957796073&partnerID=8YFLogxK
U2 - 10.1109/MEMCOD.2010.5558622
DO - 10.1109/MEMCOD.2010.5558622
M3 - Conference contribution
AN - SCOPUS:77957796073
SN - 9781424478859
T3 - 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010
SP - 49
EP - 58
BT - 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010
T2 - 8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010
Y2 - 26 July 2010 through 28 July 2010
ER -