--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on December 2009 ---
Hi, I was using ACSL in frama-c-gui. The features provided by GUI are about slicing, value analysis, dependency analysis and other static analysis options. I cannot find options for ACSL. The frama-c cmd does not seem to have such options either. How can users know if the specification written by ACSL is correct? Do we have a tutorial about how to use ACSL with frama-c or frama-c-gui? The other question is about proof backend support. Frama-C includes Caduceus http://why.lri.fr/caduceus/. Caduceus supports different backend from automatic provers and proof assistents. For example, it can generate Coq code to let users do interactive proof for tricky properties. Does Frama-C also support this? How can users generate Coq proofs from ACSL? Thanks. Jianzhou