Abstract Interpretation with the Eva Plug-in

This chapter provides an overview of the EvaEva plug-in of Frama-C, a static analyzer based on abstract interpretation, intended to automatically prove the absence of runtime errors in critical software. It aims at giving users a good understanding of how EvaEva works, by describing the theoretic principles underlying its analysis and by detailing its most important features. More practically, it also explains how to use EvaEva , set up an analysis and exploit its results.