Software Verification in Practice: Bridging Proof and Test

This research tackles a fundamental challenge in software engineering: achieving efficient and practical program verification. Traditionally, formal proofs and testing have been treated as separate—if not competing—approaches. This work proposes a unified verification strategy that transforms failed formal proofs into actionable development tools, bridging the gap between static verification and dynamic testing. 

The core innovation lies in repurposing proof failures not as dead-ends but as valuable diagnostics. When verification fails, the system generates counterexamples—human-readable descriptions of where and why the specification was violated. These counterexamples are then converted into concrete test cases, grouped to identify recurring bug patterns, or even used to propose automated program repairs. The implementation builds on tools like AutoProof and the Z3 SMT solver, which provide the underlying infrastructure for analyzing and refining failed proofs. Applications of this approach include: Automatic generation of targeted test suites (e.g., with branch or MC/DC coverage goals) Early bug detection and localization Suggestion of candidate fixes to guide program correction This research redefines the role of static verification, positioning it as a collaborative tool that supports developers rather than punishing them for failure. 

Looking ahead, future work includes extending this methodology to richer data structures and conducting usability studies to assess its effectiveness among developers with limited experience in formal methods.