A Visual Tradeoff Space for Formal Verification and Validation Techniques

Numerous techniques exist for conducting computer-assisted formal verification and validation. The cost associated with these techniques varies, depending on factors such as ease of use, the effort required to construct correct requirement specifications for complex real-world properties, and the effort associated with instrumentation of the software under test. Likewise, existing techniques differ in their ability to effectively cover the system under test and its associated requirements. To aid software engineers in selecting the appropriate technique for the formal verification or validation task at hand, we introduce a three-dimensional tradeoff space encompassing both cost and coverage.