On Sun, May 9, 2010 at 12:54 AM, Lee Pike <leep...@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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
