Follow Slashdot blog updates by subscribing to our blog RSS feed


Forgot your password?
Take advantage of Black Friday with 15% off sitewide with coupon code "BLACKFRIDAY" on Slashdot Deals (some exclusions apply)". ×

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.

6 Curses = 1 Hexahex