Follow Slashdot blog updates by subscribing to our blog RSS feed


Forgot your password?
Slashdot Deals: Cyber Monday Sale Extended! Courses ranging from coding to project management - all eLearning deals 20% off with coupon code "CYBERMONDAY20". ×

Comment Re:Just moves the errors up one level (Score 5, Interesting) 66

Once I went to a talk about applications of model checking to the verification of software. A programmer was constantly changing a state-based algorithm for call setup in a telephone switch, and was having trouble keeping it correct. Enter model checking. Two people wrote temporal specifications of call setup, and every night or so, they'd grind the model checker on the latest version of the code. No, that didn't prove the code was correct, but it did catch an enormous number of bugs in a tricky piece of concurrent code.

Oh. The programmer was Ken Thompson. The people applying the model checker were Gerard Holzmann (the designer of SPIN) and Margaret Smith.

I'm not saying the technology is applicable everywhere, but you gotta give Clarke, Emerson, and Sifakis a lot of credit for opening a good door.

"Of course power tools and alcohol don't mix. Everyone knows power tools aren't soluble in alcohol..." -- Crazy Nigel