SoylentNews is people
SoylentNews
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: 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.