You are now leaving the website that is under the control and management of DARPA. The appearance of hyperlinks does not constitute endorsement by DARPA of non-U.S. Government sites or the information, products, or services contained therein. Although DARPA may or may not use these sites as additional distribution channels for Department of Defense information, it does not exercise editorial control over all of the information that you may find at these locations. Such links are provided consistent with the stated purpose of this website.

After reading this message, click to continue immediately.

Go Back

/ Information Innovation Office (I2O)

Crowd Sourced Formal Verification (CSFV)

Crowd Sourced Formal Verification (CSFV) is a DARPA program that aims to investigate whether large numbers of non-experts can perform formal verification faster and more cost-effectively than conventional processes. The goal is to transform verification into a more accessible task by creating fun, intuitive games that reflect formal verification problems. Playing the games would effectively help software verification tools complete corresponding formal verification proofs.

Program Manager: Dr. Michael Hsieh


The content below has been generated by organizations that are partially funded by DARPA; the views and conclusions contained therein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of DARPA or the U.S. Government.

Report a problem:

Last updated: November 13, 2015

University of Illinois - Chicago Witnessing Program Transformations
University of Illinois - Chicago A Witnessing Compiler: A Proof of Concept
University of Washington Verification games: Making verification fun
University of Washington Inference and checking of object ownership
University of Washington Reducing the barriers to writing verified specifications
University of Washington ReIm & ReImInfer: Checking and inference of reference immutability and method purity
University of Washington Rely-guarantee references for refinement types over aliased mutable data
University of Washington JavaUI: Effects for controlling UI object access