Driving a sound static software analyzer with branch-and-bound - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

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

(1) , (2) , (1)
1
2

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.
Not file

Dates and versions

cea-01836516 , version 1 (12-07-2018)

Identifiers

Cite

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⟩

Collections

CEA DRT LIST
21 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More