A new move

[frvge]

Some examples why certain critical elements should be mathematically proven:

Therac 25, a computer-controlled radiation therapy machine made by Atomic Energy of Canada killed 6 people by radiation overdoses between 1985 and 1987 because of a timing problem on a data entry:
   â€œAn operator mistake could be fixed within 8 seconds, but even though the monitor reflected the operator change, the change did not affected a part of the program”

In 1994, 2 million Intel Pentium V had a bug in the FDIV operation. It could be detected by the following MS-Excel operation:
(4195835/3145727)x3145727-4195835 = 512 !!! (note by frvge: this should be 0)
Cost to Intel: $475 million
From 1994 Intel applies formal verification techniques to its products

Imagine the mainloop of the mod has a side-effect. Lateron, this can cause problems. The way to detect is, is not by simulating it 100000000000 times, because there is no guarantee that it will work at the 100000000001 time. ;) Although the chance is small... Simulation doesn't prove that the code works. This does.

[Cyntrox]

So... Tell me if I got it correct in this simplified example:

You have 2 variables, say x and y. x and y can range from 0 to 100. The verification then tries all possibilities like this:

X=0
Y=0

X=1
Y=0

X=2
Y=0

(etc)

X=99
Y=0

X=100
Y=0

X=0
Y=1

X=1
Y=1

[Overstatement]

That seems to be one of two forms of validation, this thing. I understand the what, where, when and why but how did it find those two problems? I read more into the second example and it seems that the discovery was done completely by mistake (at least on the public side, It didn't say  how Intel came to know about it).

[frvge]

@Cyntrox: no, that's simulation which is unreliable when talking about infinite sequences of numbers. There's no math involved. It's possible because of the < 100 constraint, but that'd be with model checking I think.