Edmund M. Clarke

Edmund M. Clarke 2006

Edmund "Ed" Melson Clarke, Jr. (born July 27, 1945 in Newport News , Virginia ) is an American computer scientist and Turing Prize winner . Together with Allen Emerson , he pioneered the field of model testing . Clarke is a computer science professor at Carnegie Mellon University .

Life

Clarke grew up in Smithfield , Virginia, the son of a salesman and a nurse. He studied mathematics at the University of Virginia ( Bachelor 1967) and Duke University ( Master 1968), then Computer Science at Cornell University (Master 1974 and Ph.D. with Robert Constable in 1976 with the work Completeness and Incompleteness Theorems for Hoare-like Axiom Systems ).

He then taught computer science at Duke University and went to Harvard as an assistant professor in 1978 . In 1982 he moved to the computer science department at Carnegie Mellon University and became a full professor in 1989.

Clarke researches in particular in the area of ​​software and hardware verification and machine-based evidence . In his dissertation he proved that certain control structures of programming languages did not prove their correctness well according to the Hoare calculus . In 1981 he and his first graduate student Allen Emerson proposed the use of model checking as a verification technique for finite parallel systems , and in 1982 Edmund M. Clarke implemented the first model checker, EMC .

Clarke's research group also used model testing for hardware verification for the first time. The symbolic model test using binary decision diagrams was also developed by his group (around PhD student Kenneth L. McMillan ).

Edmund Clarke was Editor-in-Chief of Formal Methods in Systems Design and serves on the editorial boards of several magazines. Together with Robert Kurshan , Amir Pnueli and Joseph Sifakis he founded the International Conference on Computer Aided Verification and is a member of their and several other program committees. Among other things, he also advised the hardware manufacturers Bolt Beranek and Newman , DEC , Fujitsu , Intel and Synopsys , and the software manufacturer Cadence Design Systems , and worked for Bell Laboratories .

Clarke also leads a multi-disciplinary, $ 10 million National Science Foundation program to establish the Institute for Model Discovery and Exploration of Complex Systems. This is intended to combine model testing and abstract interpretation under the heading MCAI 2.0 , for example to detect pancreatic cancer earlier and to learn to predict atrial fibrillation and to be able to build safer cars and airplanes. The project includes a. Amir Pnueli and James Glimm involved.

From June 11th to 14th, 2015 he took part in the 63rd Bilderberg Conference in Telfs-Buchen , Austria .

Clarke is married and has three sons.

Awards

In 2007 Clarke received the Turing Award together with Emerson and Joseph Sifakis, who also worked independently on the model test . In addition, Clarke is or was a Fellow of ACM , IEEE , Duke and Cornell University, and IBM , and has received numerous other awards, including the International Conference on VLSI Design Sidney Michaelson Best Paper Award 1991, the Semiconductor Research Corporation Technical Excellence Award 1995, the Carnegie Mellon Allen Newell Award for Excellence in Research 1999 (with Emerson), the ACM Paris Kanellakis Award 1999 (with Emerson, Randal Bryant and Kenneth L. McMillan ), the IEEE Harry H. Goode Memorial Award 2004, the Herbrand Award 2008 and the Bower Award and Prize for Achievement in Science 2014. He is a member of Sigma Xi and Phi Beta Kappa and was elected to the National Academy of Engineering in 2005 and to the American Academy of Arts and Sciences in 2011 . In 2012 he received an honorary doctorate from the Technical University of Vienna .

Fonts

• Mit Allen Emerson : Synthesis of synchronization skeletons for branching time temporal logic . In: Logic of Programs : Workshop, Yorktown Heights, NY, May 1981, Lecture Notes in Computer Science , Volume 131, Springer-Verlag. 1981.
• With JR Burch, Kenneth L. McMillan , David Dill and J. Hwang: Symbolic model checking: 10E20 states and beyond . In: LICS , 1990.

Web links

Commons : Edmund M. Clarke  - Collection of Images, Videos and Audio Files

• Clarke's website at Carnegie Mellon University (English)
• Model Checking's Role Model (PDF; 1.8 MB), The Link, issue 4.1, summer 2009, pp. 8–11, detailed report on Clarke's influence on his students, with private photos
• Role Model , Carnegie Mellon Today, Jennifer Bails, February 4, 2008

Individual evidence

1. ↑ ^{a b c} Edmund M. Clarkes Curriculum Vitae , PDF
2. ↑ ^{a b c} Edmund M. Clarke's Biographical Sketch
3. ↑ TU Vienna: Honor where honor is due!  ( Page no longer available , search in web archives )  Info: The link was automatically marked as defective. Please check the link according to the instructions and then remove this notice. . Article from January 26, 2015, accessed on March 26, 2015.  
4. ↑ TU Wien: Honorary doctorates ( memento of the original from February 21, 2016 in the Internet Archive ) Info: The archive link was inserted automatically and has not yet been checked. Please check the original and archive link according to the instructions and then remove this notice. . Retrieved March 26, 2015.