The previous chapter contains many ACSL examples; in this chapter we study a verification tool for ACSL-annotated  C programsC programs. In fact the tool used here,  Frama-CFrama-C, is closely linked to the development of ACSL. Both are being developed jointly by CEA-LIST (Software Safety and Security Laboratory) and INRIA-Saclay (Toccata team), and supported by a number of collaborative projects. More information can be obtained from the webpage of Frama-C. ACSL may well, in the future, be adopted by other verification tools for C programs.