DARPA atklāj otrās kārtas koda pārbaudes tiešsaistes spēles

ASV armijas Aizsardzības progresīvo pētījumu projektu aģentūras (DARPA) pūļa izcelsmes oficiālā verifikācijas (CSFV) eksperimenta sākumposms tika uzsākts 2013. gadā. Eksperiments tika izveidots, lai cīnītos pret dārgajām, laikietilpīgajām tradicionālo kodu verifikācijas metožu nepilnībām.

Darbojoties pie hipotēzes, ka "liels skaits ekspertu, kas nav eksperti, var veikt oficiālu verifikāciju ātrāk un rentablāk nekā parastie procesi," DARPA izstrādāja CSFV programmu, lai pārbaudītu lielas koda partijas precizitātei, izmantojot pārlūkprogrammu balstītas videospēles.

Trešdien, DARPA pasludināja programmu par veiksmīgu un paziņoja par piecu jaunu spēļu pievienošanu esošajam sastāvam. DARPA emuārā:

Šīs [2013] spēles izspēlēja spēlētāju darbības programmas anotācijās un palīdzēja oficiāliem verifikācijas ekspertiem radīt matemātiskus pierādījumus, lai pārbaudītu, vai nav svarīgu trūkumu klases "C" un "Java" programmēšanas valodās. Sākotnējā analīze liecina, ka bez ekspertiem, kas spēlē CSFV spēles, radās simtiem tūkstošu anotāciju.

Jaunie nosaukumi ietver mīklas Dynamakr, Paradokss, un Binārā skaldīšana, "zinātnes spēle" Ghost Map Hyperspaceun fantāzijas sim Monster pierādījums. Visas DARPA CSFV spēles, tostarp no 2013. gada projekta fāzes, ir pieejamas tiešsaistē Verigames. Lai piedalītos, spēlētājiem jābūt 18 gadus veciem vai vecākiem.