Plug-in proof support for formal development environments
David Hemer, Gregory J. Long, Paul A. Strooper · 2005
A number of industrial software development standards mandate that safety-critical software components be developed using formal methods, including formal verification. While formal development is supported by a number of formal development environments, verification of correctness properties is still a major bottleneck. Most formal development environments provide built-in facilities for discharging these correctness properties (so-called proof obligations). However these built-in tools are typically less mature and sophisticated than stand-alone theorem provers. FDEs would benefit from being able to use a variety of theorem provers to discharge proof obligations, where di#erent provers can be selected for di#erent problem domains.