Driving Frama-C's Value Analysis Towards a User Specified Goal
SPALTER is a Frama-C plug-in that iteratively improves the precision of Frama-C's value analysis results. It uses a variation of the Skelboe-Moore algorithm from the field of interval arithmetic and instructs Frama-C to execute case analyses that reintroduce previously ignored relations.
Although SPALTER currently only exists as a prototype, it automatically reproduces two Frama-C case studies (I, II), one of which required significant user interaction.
SPALTER was initially created during an internship of Sven Mattsen with the CEA List, supervised by Pascal Cuoq.
