Driving a sound static software analyzer with branch-and-bound - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

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

Résumé

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.
Fichier non déposé

Dates et versions

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

Identifiants

Citer

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⟩
22 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More