[barries]

See also Frama-C (http://frama-c.com/), which can use multiple automated and interactive theorem provers. It's really a proof obligation management IDE that you can use with multiple provers / proof assistants.