Become a fan of Slashdot on Facebook

 



Forgot your password?
typodupeerror
×
Bug Software The Military Games

DARPA Wants You To Verify Software Flaws By Playing Games 31

coondoggie writes: Researchers at the Defense Advanced Research Projects Agency (DARPA) think online gamers can perform the tedious software verification work typically done by professional coding experts. They were so impressed with their first crowdsourced flaw-detecting games, they announced an new round of five games this week designed for improved playability as well as increased software verification effectiveness. “These games translated players’ actions into program annotations and assisted formal verification experts in generating mathematical proofs to verify the absence of important classes of flaws in software written in the C and Java programming languages. An initial analysis indicates that non-experts playing CSFV games generated hundreds of thousands of annotations,” DARPA stated.
This discussion has been archived. No new comments can be posted.

DARPA Wants You To Verify Software Flaws By Playing Games

Comments Filter:
  • War Games (Score:4, Funny)

    by Stuarticus ( 1205322 ) on Friday May 29, 2015 @06:57AM (#49797713)
    Set number of players zero.
  • by Anonymous Coward

    ./ --

    Run this article, respond appropriately and this protest will be over. You're acticting like a manager/laywer-type person at Oracle. You can do better than this.

    This is "the" scandal in tech right now, and you're actively supressing discusstion --

    http://mobile.slashdot.org/comments.pl?sid=7477721&cid=49793333 [slashdot.org]

    Mod this up like all the other SF posts, please.

    http://arstechnica.com/information-technology/2015/05/sourceforge-grabs-gimp-for-windows-account-wraps-installer-in-bundle-pushing-adware/ [arstechnica.com]

    Sourc

  • This is way over my head. I read the link, and got a grasp of the concept.
    but I want to learn more.
    Does anyone have something more detailed I could read and learn with ??
    thanks in advance.

    • by JimWhiteheadUCSC ( 4131419 ) on Friday May 29, 2015 @12:41PM (#49800391) Homepage

      I'm one of the people involved in creating the Binary Fission game, so I can explain a little bit about what is going on "behind the scenes" in this game.

      In Binary Fission (http://binaryfission.verigames.com/), players use filters to try and make clean separations between piles of blue and gold colored dots ("bits"). It is usually the case that no one filter cleanly separates all of the blue bits from the gold bits, and hence solving a puzzle requires judicious use of filters to subdivide the piles into smaller piles, until you can find filters that do cleanly separate the smaller piles.

      Overall, the science goal of the game is to have players discover "loop invariant" conditions (http://en.wikipedia.org/wiki/Loop_invariant). This is a mathematical expression that describes (an approximation to) the behavior of a loop (for loop, while loop). For example, if a loop increments x by two each time through the loop, then a loop invariant would be x = {initial value of x} + {loop iteration count} * 2. At any point in the execution of the loop, this condition always holds. That is, the condition doesn't vary, and is "invariant".

      Behind the scenes, each of the bits (the dots) really represents a cluster of mappings of variables to values within a single iteration through a loop. One color of bits represents values of variables that are "good" -- they are consistent with the values that variables could have during loop execution. The other color of bits represents values of variables that are "bad" -- they are values that the variables could never have during loop execution.

      The filters represent possible loop invariant conditions. A strong loop invariant condition will perfectly separate the good values from the bad values, and thereby be a precise description of the behavior of the loop. Multiple combinations of filters can be combined together to create an aggregate loop invariant expression.

      One way of putting this is we're looking at finding loop invariants as a kind of classification problem, where we're trying to find the best possible classifier that will separate valid variable values from invalid variable values. The act of applying filters involves the player constructing a classifier.

      Right now, the filters in Binary Fission are candidate loop invariants that are output by the Daikon automated loop invariant finder (http://plse.cs.washington.edu/daikon/). These candidate invariants from Daikon are not usually good enough to describe the entire loop behavior, so the human player is using their unique judgement to augment the best output we get from automated invariant finder tools.

      • What a great Response, had to read it 3 times before I could get a basic grasp...
        What a cool idea all this is, play a game and somehow ( I know you explained it, but still don't grasp it all )
        it helps out solving something.

        Keep up the great Ideas and work

      • I ran through a couple rounds of your game. I'm not trying to knock it, but if I may ask an ignorant question: If a computer can determine the value of structures created by a human, couldn't the computer generate structures and evaluate them much, much faster than a human (or even as many humans as you can muster to play the game)?
  • I tried Paradox. No idea what's going on. Click, drag, click, something happens. Yay! What?

    I tried dynamakr as well. Even less of a clue. "Left Seek Similar Patterns!" "Enhance Energy!" And then it turns into some weird shoot 'em up. It feels like the game equivalent of a book translated from Swahili to English via Japanese.

  • Let's get players to play tic-tac-toe, and we'll use the unique GameID they generate to annotate a number line to make a mathematical proof that the number line is infinite in the positive direction!
  • Why did Dice buy Slashdot? [dice.com]

    So they could [arstechnica.com] suppress discussions [reddit.com] about their own [filezilla-project.org] scandals! [sdtimes.com]

    SHAME ON YOU DICE!
  • Why should I be free labor. Nobody rides for free....

  • They need to fix their games so that you can actually play them. I tried some of them and one wouldn't run at all under IE, so I ran it under Chrome and got a little bit farther. That ones Monster Proof. I forget which one threw a dialog box error after getting through the first level and clicking Go to Next Level. Then there was one with text too small. Another had a light grey on dark grey thing for text and a glow around the text.

Think of it! With VLSI we can pack 100 ENIACs in 1 sq. cm.!

Working...