Edmund M. Clarke facts for kids
Quick facts for kids
Edmund M. Clarke
|
|
|---|---|
 |
|
| Born |
Edmund Melson Clarke, Jr.
July 27, 1945 Newport News, Virginia, U.S.
|
| Died | December 22, 2020 (aged 75) Pittsburgh, Pennsylvania, U.S.
|
| Nationality | American |
| Alma mater | Cornell University |
| Known for | Model checking |
| Awards | A.M. Turing Award |
| Scientific career | |
| Fields | Computer science |
| Institutions | Carnegie Mellon University |
| Thesis | Completeness and Incompleteness Theorems for Hoare-Like Axiom Systems (1976) |
| Doctoral advisor | Robert Lee Constable |
| Doctoral students |
|
Edmund Melson Clarke, Jr. (born July 27, 1945 – died December 22, 2020) was an American computer scientist. He was well-known for creating a method called model checking. This method helps check if computer hardware and software designs work correctly.
He was a professor of Computer Science at Carnegie Mellon University. In 2007, Clarke, along with E. Allen Emerson and Joseph Sifakis, received the important Turing Award. This award is like the Nobel Prize for computer science.
Contents
About Edmund Clarke
Edmund Clarke was born in Newport News, Virginia. He loved mathematics and computer science.
His Education
He earned his first degree in mathematics from the University of Virginia in 1967. Then, he got another degree in mathematics from Duke University in 1968.
He later earned his Ph.D. (a very high degree) in Computer Science from Cornell University in 1976.
His Career
After finishing his studies, he taught at Duke University for two years. In 1978, he moved to Harvard University as a computer science professor.
In 1982, he joined Carnegie Mellon University in Pittsburgh. He became a full professor there in 1989. In 1995, he received a special professorship called the FORE Systems Professorship. He became an emeritus professor in 2015.
Edmund Clarke passed away in December 2020 at the age of 75.
What He Did
Edmund Clarke was very interested in making sure computer programs and parts (hardware) worked perfectly. He also worked on automatic theorem proving, which means teaching computers to solve logic problems.
Model Checking
In 1981, he and his student E. Allen Emerson came up with the idea of model checking. This was a new way to check if complex computer systems worked as they should.
His research group was the first to use model checking to test computer hardware. They also developed a smart way to do model checking using something called "binary decision diagrams."
Other Inventions
His team also created the first computer program that could solve many logic problems at once (called Parthenon). They also made the first program that could solve math problems using symbols (called Analytica).
In 2009, he helped start a center called CMACS. This center brings together researchers from different universities. They use advanced computer methods to study complex systems, like those in biology.
Awards and Honors
Edmund Clarke received many awards for his important work.
- He was a fellow of the ACM and the IEEE. These are important groups for computer scientists.
- In 1999, he won the ACM Paris Kanellakis Award. He shared this award for developing symbolic model checking.
- In 2004, he received the IEEE Computer Society Harry H. Goode Memorial Award. This was for his major contributions to checking hardware and software.
- He was elected to the National Academy of Engineering in 2005. This is a very high honor for engineers.
- In 2007, he received the Turing Award, one of the highest honors in computer science.
- He also received the Herbrand Award in 2008 for his role in creating model checking.
- In 2014, he won the Bower Award and Prize for Achievement in Science from the Franklin Institute. This was for his leading role in making sure computer systems work correctly.
See also
In Spanish: Edmund Clarke para niños
