[edwcross]

Funny you mentioned TrustInSoft but not its open-source origin (which is still under development and evolving in a different direction), Frama-C. I cannot compare it to IKOS, but their usefulness depends a lot on the type of code and verification needs.

[AlotOfReading]

I want to like Frama-C, but I've never managed to actually use it successfully on real projects and the repeated experiences have soured me on it. Getting a recent version installed was a serious chore last time I tried, and no one else is willing to deal with ACSL to get the full value.

[KsassPeuk]

At some point in the past you also posted the ACSL cast badly documented. I asked you what you needed exactly, but you probably missed the message. So let me try again:

What kind of documentation would you expect in addition to ACSL by Example and the WP tutorial?