Driving a sound static software analyzer with branch-and-bound

Abstract : 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.
Document type :
Conference papers
Complete list of metadatas

https://hal-cea.archives-ouvertes.fr/cea-01836516
Contributor : Léna Le Roy <>
Submitted on : Thursday, July 12, 2018 - 1:24:41 PM
Last modification on : Wednesday, January 23, 2019 - 2:39:33 PM

Identifiers

Collections

CEA | DRT | LIST

Citation

S. Mattsen, P. Cuoq, S. Schupp. Driving a sound static software analyzer with branch-and-bound. 2013 IEEE 13th International Working Conference on Source Code Analysis and Manipulation (SCAM), Sep 2013, Eindhoven, Netherlands. pp.63-68, ⟨10.1109/SCAM.2013.6648185⟩. ⟨cea-01836516⟩

Share

Metrics

Record views

61