In conclusion (part 1)
- Frama-C is a real open source tool.
- Not as hard to use as I imagined.
- Mostly useful for small functions.
→ For large functions look at constructive proofs in WhyML.
- Forces you to think very hard about assumptions and corner cases.
- Very well documented, questions answered quickly on stackoverflow.