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.