The Association for Computing Machinery has given it\s highly prestigious A.M. Turing Award to the researchers credited for inventing Model Checking: Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis.

I believe it was in the 1960s that a few computer science pioneers such as Edsger Dijkstra suggested checking computer programs through formal proofs. For instance, it's obvious you'd better be careful if you write code such as: 


if ( var > 0 )
  func();
else if ( var = 0 )
  return;
Any programmer looking at that has to ask: what does the program do if var is less than 0? Is it OK if the program just falls through to the next statement? If not, can you be sure that var can never be less than 0 when the program reaches this point? These sort of questions are what formal proofs are supposed to expose and resolve.

Formal proofs looked great for academic exercises, but quickly became untenable when applied to real-life applications because of the explosion of possible states. The same originally was true for Model Checking when it was invented in the 1980s.

Another problem with these systems is that they beg the question of whether a program is correct. You can't run a proof without specifying your requirements in a highly formal manner, and the formal statement could just as easily have a bug as the program you want to check, a qui custodiat custos situation.

Gradually these problems were overcome to enough of an extent that Model Checking proves useful in a wide range of situations nowadays, and a huge number of products support it. It's particularly useful in hardware, probably because you're not facing the irony of using code to check code (the qui custodiat custos situation).

So computer science can solve some of the big problems in quality. Congratulations to the honored researchers.