2013年に開始された米国陸軍の国防高等研究計画局(DARPA)クラウドソース形式検証(CSFV)実験の初期段階。この実験は、伝統的なコード検証方法の高価で時間のかかる落とし穴を克服するために作成されました。
DARPAは、「多数の非専門家が従来のプロセスよりも迅速かつ低コストで正式な検証を実行できる」という仮説に基づいて、ブラウザベースのビデオゲームを使用して大量のコードの正確性をチェックするように設計しました。
水曜日、DARPAはこのプログラムの成功を宣言し、5つの新しいゲームを既存のラインナップに追加することを発表しました。 DARPAブログから:
これらの[2013]ゲームは、プレーヤーの行動をプログラムの注釈に変換し、 "C"および "Java"プログラミング言語に重要な種類の欠陥がないことを検証するための数学的証明の生成において形式検証の専門家を支援しました。最初の分析では、CSFVゲームをプレイしている非専門家が何十万もの注釈を生成したことを示しています。
新しいタイトルにはパズルが含まれています ダイナマクル, 逆説、そして 二分裂科学ゲーム ゴーストマップハイパースペース、そしてファンタジーシム モンスタープルーフ。 2013年プロジェクト段階のものも含め、DARPAのCSFVゲームはすべてVerigamesでオンラインで入手できます。参加するには、ゲーマーは18歳以上でなければなりません。