Numerical stability analysis of floating-point computations using software model checking

Franjo Ivančić, Malay K. Ganai, Sriram Sankaranarayanan, Aarti Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Scopus citations

Abstract

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.

Original languageEnglish (US)
Title of host publication8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010
Pages49-58
Number of pages10
DOIs
StatePublished - Oct 15 2010
Externally publishedYes
Event8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010 - Grenoble, France
Duration: Jul 26 2010Jul 28 2010

Publication series

Name8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010

Other

Other8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010
CountryFrance
CityGrenoble
Period7/26/107/28/10

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Hardware and Architecture
  • Software

Fingerprint Dive into the research topics of 'Numerical stability analysis of floating-point computations using software model checking'. Together they form a unique fingerprint.

Cite this