Options
Driving a sound static software analyzer with branch-and-bound
Publikationstyp
Conference Paper
Publikationsdatum
2013
Sprache
English
Institut
TORE-URI
Start Page
63
End Page
68
Article Number
6648185
Citation
2013 IEEE 13th International Working Conference on Source Code Analysis and Manipulation (SCAM 2013) : Eindhoven, Netherlands, 22 - 23 September 2013 / [sponsors: IEEE Computer Society Technical Council on Software Engineering ... Ed.: Bram Adams ...]. - Piscataway, NJ : IEEE, 2013. - Art.-Nr. 6648185, i.e. Seite 63-68
Contribution to Conference
Publisher DOI
Scopus ID
Publisher
IEEE
During the last decade, static analyzers of source code have improved greatly. Today, precise analyzers that propagate values for the program's variables, for instance with interval arithmetic, are used in the industry. The simultaneous propagation of sets of values, while computationally efficient, is a source of approximations, and ultimately of false positives. When the loss of precision is detrimental to the user's goals, a user needs to provide some kind of manual guidance. Frama-C, a framework for the static analysis of C programs, provides a sound value analyzer. This analyzer can optionally be guided by skillfully placed user annotations. This article describes SPALTER, a Frama-C plug-in that uses a variation of the Skelboe-Moore algorithm from the field of interval arithmetic to guide Frama-C's value analyzer towards a high-level objective set by the user. SPALTER reproduces the results of a case study that used Frama-C's value analysis and required extensive manual guidance. In difference, our approach with SPALTER required no guidance, except preparation of the analyzed program by slicing. © 2013 IEEE.
DDC Class
600: Technik
620: Ingenieurwissenschaften