Online gaming is popular and it would be extremely valuable if a system could harness this intellectual effort for practical purposes. In this report, we discuss two crowd-sourced, on-line games, that present players with arcade-style puzzles to solve. The puzzles in Ghost Map and Ghost Map Hyperspace are generated from a formal analysis of the correctness of a software program. In our approach, a puzzle is generated for potential flaws in the software and the crowd produces formal proofs of the softwares correctness by solving the puzzles. This report documents the challenges, lessons learned and efficiency of producing formal verification proofs of software through crowd sourced game play.
This was a neat experiment by DARPA with a quick summary here. The site with the games is here. I couldn’t play them for some reason the few times I tried. kel has motivated me to try again to fire up some games in the name of secure software. :)
They’re not working. CPU fan is. (sighs) Screw it. Still cool paper and project. Least there’s a YouTube channel so we can try to see footage of the games. Found a video of this game. Enjoy! :)
Ah neat, I know some people who worked on the UC Santa Cruz part of this DARPA games-for-verification thing; didn’t realize it was a bigger multi-institution initiative. Their game was Xylem: The Code of Plants (paper, video).
Software not working but the heater under your desk remaining hard at work pumping out hot air is an age-old signature of not only the game industry but of computer science academia lol
Thank you, for the helpful links.
Tell me about it lol. I just semi-revived my old laptop in case a mix of CPU-heavy dev tools and web pages kills my current one prematurely. I wish I was joking but I think a Celeron with fan raging on web pages whose games aren’t running just isnt sustainable. ;)