Edmund Clarke, informatician american

Edmund Melson Clarke Jr. (27 iulie 1945 – 22 decembrie 2020) a fost un informatician american renumit pentru dezvoltarea modelului de verificare, o metodă de verificare formală a design-urilor hardware și software. A fost profesor de informatică FORE Systems la Universitatea Carnegie Mellon. Clarke, împreună cu E. Allen Emerson și Joseph Sifakis, a primit premiul ACM Turing în 2007.

Născut în Newport News, Virginia, Clarke a obținut o diplomă de licență în matematică la Universitatea Virginia din Charlottesville în 1967, un master în matematică la Universitatea Duke din Durham, NC, în 1968 și un doctorat în Informatică la Universitatea Cornell din Ithaca, NY, în 1976. După finalizarea doctoratului, a predat timp de doi ani la Departamentul de Informatică al Universității Duke. În 1978, a devenit profesor asistent la Universitatea Harvard, în cadrul Diviziei de Științe Aplicate. A părăsit Harvard în 1982 pentru a se alătura Departamentului de Informatică al Universității Carnegie Mellon din Pittsburgh, PA, unde a devenit profesor titular în 1989 și a primit titlul de profesor FORE Systems în 1995. În 2008, a devenit profesor universitar, iar în 2015 a fost numit profesor emerit.

Clarke a murit în decembrie 2020, la vârsta de 75 de ani, în timpul pandemiei din Pennsylvania.

Sursa foto: https://ro.wikipedia.org/wiki/Edmund_Clarke#/media/Fi%C8%99ier:Edmund_Clarke_FLoC_2006.jpg

Interesele sale de cercetare au inclus verificarea software-ului și hardware-ului, precum și demonstrarea automată a teoremelor. În teza sa de doctorat, a arătat că anumite structuri de control ale limbajelor de programare nu pot fi demonstrate eficient în stilul Hoare. În 1981, împreună cu studentul său E. Allen Emerson, a propus pentru prima dată utilizarea verificării modelelor ca metodă de verificare a sistemelor concurente cu stări finite. Grupul său de cercetare a fost un pionier în utilizarea verificării modelelor pentru verificarea hardware-ului, iar verificarea modelelor simbolice utilizând diagrame de decizie binare a fost dezvoltată de echipa sa. Această tehnică a fost subiectul tezei de doctorat a lui Kenneth McMillan, care a câștigat premiul pentru teza sa de doctorat ACM. De asemenea, grupul său a dezvoltat Parthenon, primul demonstrator de teoreme de rezoluție paralelă, și Analytica, un demonstrator de teoreme bazat pe un sistem de calcul simbolic.

În 2009, a condus crearea Centrului de Modelare și Analiză a Sistemelor Complexe (CMACS), finanțat de Fundația Națională pentru Știință. Acest centru a adunat o echipă de cercetători din mai multe universități, care aplicau interpretarea abstractă și verificarea modelelor pentru sistemele biologice și încorporate.

Clarke a fost membru al ACM și IEEE. În 1995, a primit un premiu de excelență tehnică din partea Semiconductor Research Corporation, iar în 1999, împreună cu Randal Bryant, E. Allen Emerson și Kenneth McMillan, a câștigat premiul ACM Paris Kanellakis pentru dezvoltarea verificării simbolice a modelelor. În 2004, a primit premiul IEEE Computer Society Harry H. Goode Memorial Award pentru contribuțiile sale semnificative în verificarea formală a sistemelor hardware și software, iar în 2005 a fost ales membru al Academiei Naționale de Inginerie. În 2011, a fost ales membru al Academiei Americane de Arte și Științe.

A primit premiul Herbrand în 2008 pentru inventarea verificării modelelor și pentru conducerea sa de succes în acest domeniu timp de mai bine de două decenii. În 2012, i s-a acordat un doctorat onorific de la TU Wien, iar în 2014 a primit premiul Bower pentru realizări în știință din partea Institutului Franklin, în recunoașterea rolului său important în dezvoltarea tehnicilor de verificare automată a corectitudinii sistemelor informatice. De asemenea, a fost membru al Sigma Xi și Phi Beta Kappa.

Sursa: https://ro.wikipedia.org/wiki/Edmund_Clarke