Die Anfangsphase des Crowd-Sourcing-Experiments zur formalen Verifizierung (CSFV) der US Army Defence Advanced Research Projects Agency (DARPA), das 2013 gestartet wurde. Das Experiment wurde erstellt, um die teuren, zeitaufwändigen Fallstricke herkömmlicher Methoden zur Code-Verifizierung zu bekämpfen.
Ausgehend von der Hypothese, dass "eine große Anzahl von Nicht-Experten eine formale Verifizierung schneller und kostengünstiger durchführen kann als herkömmliche Prozesse", entwickelte DARPA das CSFV-Programm, um große Mengen von Code mithilfe von browserbasierten Videospielen auf ihre Richtigkeit zu überprüfen.
Am Mittwoch verkündete DARPA den Erfolg des Programms und kündigte die Hinzufügung von fünf neuen Spielen zu seiner bestehenden Aufstellung an. Aus dem DARPA-Blog:
Diese [2013] -Spiele übersetzten die Aktionen der Spieler in Programmanmerkungen und halfen formalen Überprüfungsexperten dabei, mathematische Beweise zu erstellen, um das Fehlen wichtiger Fehlerklassen in den Programmiersprachen "C" und "Java" zu überprüfen. Eine erste Analyse zeigt, dass Nicht-Experten, die CSFV-Spiele spielen, Hunderttausende von Anmerkungen generiert haben.
Die neuen Titel beinhalten Puzzler Dynamakr, Paradox, und Zellteilung, "Wissenschaftsspiel" Ghost Map Hyperraumund Fantasie sim Monster Beweis. Alle CSFV-Spiele von DARPA, einschließlich der aus der Projektphase 2013, sind online bei Verigames erhältlich. Spieler müssen mindestens 18 Jahre alt sein, um teilnehmen zu können.