Crowd-Sourced Help with Emergent Knowledge for Optimized Formal Verification (CHEKOFV)
Jim Murray, Jim Whitehead, Florent Kirchner · 2016
Formal Verification of Software is an expensive and time consuming task aimed at discovering and correcting software errors that lead to programming errors. The Crowd-Sourced Formal Verification CSFV program was developed to explore utilizing games to prove correctness proofs for software. Leveraging human pattern recognition skills, the CSFV games provide formal verification proofs a machine analyzing the code cannot. The SRI team developed two games Xylem The Code of Plants, and Binary Fission to prove Crowd Sourced game play can improve Formal Verification effectiveness and reduce the cost to verify code.