The Man Who Proved Systems Could Be Trusted

And as you said, Joseph, at that time, nineteen seventies, you had that idea.

This type of operations for systems would be very complex and would require a lot of compute power, which wouldn't exist, right, in ninety-seven?

Right.

How do you explain it? How do you explain it? Was this intuition?

No, no. Y-yes, okay.

I like mathematics.

I liked model or logic.

So I built a theory, and the theory was just an intellectual construction, okay? I remember when I passed my PhD, some people in the jury said, "But this theory is not applicable, okay? It's a nice theory.

It's not applicable." So I was unable to put my theory in practice, but this w-was a nice theoretical result More powerful machines that were not available at that time, I could apply my theory, okay? So I had to wait until computer performance improved, and also I should say that the need for verification became increasingly urgent because people were developing also increasingly complex systems.

So in nineteen ninety-four, I launched the first Pentium, uh, processor.

So this processor had a problem.

It had a failure, but the failure was an intermittent failure, and it was poorly understood why this appeared, and it was very hard to reproduce, to reproduce through testing.

At that time, of course, Intel's reputation was, uh, at stake and, and also-

Mm-hmm

... a lot of money.

Okay? And Intel decided to invest heavily in the development of the first industrial scale, uh, technology based on model checking.

I think they were successful.

They never told me what they achieved.

Intel's example was immediately followed by other developers of critical systems, NASA, IBM, and Microsoft, and later.

That's very impressive.

Practically, today, what are applications that we might be using or computer scientists might be using and are leveraging on model checking?

There are many, many applications.

It's applied to hardware, to critical software because you see applying model checking techniques costs a lot of money.

You need also a very high performance computers.

You don't try to verify a software that you will use it for non-critical tasks.