Edmund M. Clarke, the FORE Systems Professor of Computer Science Emeritus at Carnegie Mellon University, has died of Covid-19.
Obituary: Edmund M. Clarke, CMU professor who won computer science's Nobel Prize equivalent:
Edmund M. Clarke, a professor emeritus at Carnegie Mellon University who won computer science's equivalent of the Nobel Prize, died Tuesday of COVID-19 after a long illness. He was 75.
[...] In the early 1980s, Mr. Clarke and his Harvard University graduate student, E. Allen Emerson — as well as Joseph Sifakis of the University of Grenoble, who was working separately — developed model checking, which has helped to improve the reliability of complex computer chips, systems and networks.
For their work, the Association for Computing Machinery gave the three scientists the prestigious A.M. Turing Award — computer science's Nobel Prize — in 2007.
Mr. Clark's citation[*] on the Turing Award website[**] said Microsoft and Intel and other companies use model checking to verify designs for computer networks and software.
"It is becoming particularly important in the verification of software designed for recent generations of integrated circuits, which feature multiple processors running simultaneously," the citation page said. "Model checking has substantially improved the reliability and safety of the systems upon which modern life depends."
Model checking allowed engineers to analyze the logic beneath a design similar to how a mathematician uses a proof to determine that a theorem is correct, according to CMU. It considers every possible state of a hardware or software design and determines if it is consistent with the designer's specifications.
Before the development of model checking, CMU said, engineers checked for logic errors in computer circuitry or software programs by running simulations to test performance as well as manually examining each line of computer code. But those methods became inadequate as computers became more complex, and errors often went undetected until after a product was released, which could be costly even when minor, according to the university.
[*] https://amturing.acm.org/award_winners/clarke_1167964.cfm
[**] https://amturing.acm.org/
(Score: 1, Funny) by Anonymous Coward on Tuesday December 29 2020, @03:22AM (1 child)
I went to his prize lecture (in 2007?) and loaded up on food at the reception afterward. He looked at me like I was a freeloader :)
RIP. his talk was very interesting on the topic of state explosion.
(Score: 0) by Anonymous Coward on Tuesday December 29 2020, @07:50AM
But how was the sursild?
(Score: -1, Troll) by Anonymous Coward on Tuesday December 29 2020, @03:42AM (1 child)
Like the one Obama got for nothing? Or the one they gave to the guy who invented PCR who said you can't use it to test for a virus?
(Score: -1, Offtopic) by Anonymous Coward on Tuesday December 29 2020, @03:56AM
Nope, none of those.
The one Bob Dylan got for literature/poetry.
(Score: 4, Insightful) by Thexalon on Tuesday December 29 2020, @04:32AM (5 children)
If we're going to make the ACM Turing Award as famous as, say, the Fields Medal or the Nobel Prize, we should be clear that it's not "the equivalent of the Nobel", but an awesome achievement in its own right. And it's not like there aren't absolute greats who have received it (Ken Thompson comes to mind - nothing big, just a guy whose ideas power the vast majority of computers in the world today).
Particularly on a site where people ought to know what that award is.
The only thing that stops a bad guy with a compiler is a good guy with a compiler.
(Score: 0) by Anonymous Coward on Tuesday December 29 2020, @07:48AM (4 children)
If his model checking is so good, why does my code still have bugs?
(Score: 0) by Anonymous Coward on Tuesday December 29 2020, @02:11PM
Most people are broadly incompetent and poorly match their talents and profession. As most producers are incompetent to the task, and consumers incompetent to judge the product, it doesn't become widely known that something sucks until everybody has it. Incompetent producers iterate, building on top of incompetence, and you get to where we are. The best ideas don't win, because there aren't enough competent people, talented in their field, to think of those solutions before the problems are obsolete or deeply entrenched.
(Score: 2) by Thexalon on Tuesday December 29 2020, @04:04PM (1 child)
The real answer: Because this work was focused on ensuring the bugs in your code weren't caused by your CPU - it doesn't protect you from your own mistakes.
The only thing that stops a bad guy with a compiler is a good guy with a compiler.
(Score: 0) by Anonymous Coward on Wednesday December 30 2020, @12:43AM
When I studied digital systems design, formalized model checking was used for only the most simple of designs that could then be combined - the state explosion problem makes full model checking impractical.
AFAIK, verification work comprises the majority of the man hours going in to design a CPU/GPU. Designing test regimens and vectors is what they do - that doesn't sound quite so provable to me as model checking promises.
(Score: 0) by Anonymous Coward on Friday January 01 2021, @11:18AM
No wonder your code has bugs.
(Score: 2) by choose another one on Tuesday December 29 2020, @05:08PM (3 children)
I guess that's a US thing, this side of the pond you only get to die of COVID after a short (28 days) illness, if it's a long illness you are considered ipso-facto recovered...
Actually maybe it's not a geographical issue, but a type definition / conversion issue - in the end a model checking failure. RIP.
(Score: 0) by Anonymous Coward on Tuesday December 29 2020, @05:20PM (2 children)
He was old in 2007, and emeritus by then. Obviously, he had a long term illness like cancer, and he died in the hospital with the virus, so they got to claim it as a covid death for the bonus.
(Score: 0) by Anonymous Coward on Tuesday December 29 2020, @07:33PM (1 child)
Automobile accidents are grossly overcounted in the same manner. For instance, those people who die in a crash on their way to the hospital for their chemo treatment, their car crash really just exasperated their underlying cancer condition and they should properly be tabulated as a cancer death.
Come to think of it, cancer deaths are overcounted too. People with cancer have old age as an underlying condition (whether they die at 9 or 90), which they were going to die of anyway, but as a bonus it gets tabulated as a cancer death.
(Score: 0) by Anonymous Coward on Tuesday December 29 2020, @10:33PM
When I said bonus, I meant in the green dollars sense. Hospitals get money from the government for covid deaths. Increased cancer counts may indirectly get them donations.