[Haskell-cafe] Re: Frama-C

[Tom Hawkins]

On Sun, May 9, 2010 at 12:54 AM, Lee Pike <leepike at gmail.com> wrote:
> Tom,
>
>> Have you used any of these tools?  They're pretty cool.  I'd be
>> interested to hear you opinion.
>>
>> http://frama-c.com/
>
> Not yet.  We were considering using them for a C security-analysis, but
> rolled-our-own stuff in Haskell.

Do you guys support ACSL or something similar?

One major short comings of Frama-C is its inability to prove a formula
false.  As such, the tool will not return any counter examples to help
with debugging.

>
> I'll ask around Galois if there's been any experience with it.
>
> Did anyone respond to your post about a Haskell interface?

Negative.

I'm looking into writing a bit of OCaml to dump out the Cil+ACSL
stuff, which I can then read with Haskell.

One thing I really like about Frama-C is its use of multiple solvers.
Some work better than others, and it's very easy to see this in the
gWhy GUI, as well as overall proof coverage.

It would be nice to have a Haskell library where we could stream in a
bunch of proof obligations and it would farm it out to different
solvers, possibly running on different machines.  It could also keep
track of which obligations have proved true or false, so it doesn't
wast time running the obligation on other solvers -- gWhy doesn't
currently do this.

You kind of alluded to these benefits when you recommended using
SMT-LIB instead of Yices for AFV, but I didn't appreciated it until
now.

-Tom