You are now leaving the DARPA.mil 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.
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: firstname.lastname@example.org
Last updated: November 13, 2015
|University of Illinois - Chicago||Witnessing Program Transformations||Not Yet Published|
|University of Illinois - Chicago||A Witnessing Compiler: A Proof of Concept||Not Yet Published|
|University of Washington||Verification games: Making verification fun||http://homes.cs.washington.edu/~mernst/pubs/verigames-ftfjp2012-abstract.html|
|University of Washington||Inference and checking of object ownership||http://homes.cs.washington.edu/~mernst/pubs/infer-ownership-ecoop2012-abstract.html|
|University of Washington||Reducing the barriers to writing verified specifications||http://homes.cs.washington.edu/~mernst/pubs/veriweb-oopsla2012-abstract.html|
|University of Washington||ReIm & ReImInfer: Checking and inference of reference immutability and method purity||http://homes.cs.washington.edu/~mernst/pubs/infer-refimmutability-oopsla2012-abstract.html|
|University of Washington||Rely-guarantee references for refinement types over aliased mutable data||http://homes.cs.washington.edu/~mernst/pubs/rely-guarantee-ref-pldi2013-abstract.html|
|University of Washington||JavaUI: Effects for controlling UI object access||http://homes.cs.washington.edu/~mernst/pubs/gui-thread-ecoop2013-abstract.html|