Boris Yakobowski

Joint work with Sandrine Blazy and David Bühler.

In this paper, we present a generic abstract interpretation based framework to enhance the precision of analyses on codes containing multiple successive conditionals. We introduce predicated domains, that preserve and reuse information valid only inside some branches of the code. Our predicates, derived from the conditional statements of the program, postpone the loss of information caused by joins.

The work has been integrated into Frama-C as a new plugin. Experiments on real code show that our approach scales, and improves significantly the precision of the Value Analysis plugin of Frama-C.

This article has been published in the proceedings of FMICS 2014, where it was awarded the best paper award. Here are the pdf and the link at the publisher's website. A journal version is under consideration for publication.

Coq proofs of the results in the journal version: .v file, or as an html page.