Skip to main content

2014 | OriginalPaper | Buchkapitel

Practical Floating-Point Tests with Integer Code

verfasst von : Anthony Romano

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer Berlin Heidelberg

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Testing integer software with symbolic execution is wellestablished but floating-point remains a specialty feature. Modern symbolic floating-point tactics include concretization, lexical analysis, floating-point solvers, and intricate theories, but mostly ignore the default integer-only capabilities. If a symbolic executor is already highperformance, then software-emulation, common to integer-only machines, becomes a compelling choice for symbolic floating-point.

We propose a software floating-point emulation extension for symbolic execution of binary programs. First, supporting a soft floating-point library requires little effort, so multiple models are cheap; our executor has five distinct open source soft floating-point code bases. For integrity, test cases from symbolic execution of library code itself are hardware validated; mismatches with hardware appear in every tested library, a justin- time compiler, a machine decoder, and several floating-point solvers. In practice, the executor finds program faults involving floating-point in hundreds of Linux binaries.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Metadaten
Titel
Practical Floating-Point Tests with Integer Code
verfasst von
Anthony Romano
Copyright-Jahr
2014
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-642-54013-4_19

Premium Partner