[AlotOfReading]

Astree is a pain in the butt. Even if it were free, I'd recommend it to very few people. It's not usable without someone (often a team) being responsible for it full time.

TrustInSoft is the higher quality option, polyspace is the more popular option, and IKOS is probably the best open source option. I've also had luck with tools from Galois Inc and the increasingly dated rv-match tool.

[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?

[ryao]

Tell me more.