Knowledge (XXG)

Edmund M. Clarke

Source 📝

36: 104: 1845: 645:
for "his leading role in the conception and development of techniques for automatically verifying the correctness of a broad array of computer systems, including those found in transportation, communications, and medicine." He was a member of
1890: 616:
Memorial Award for significant and pioneering contributions to formal verification of hardware and software systems, and for the profound impact these contributions have had on the electronics industry. He was elected to the
1870: 535:(Parthenon) and a theorem prover based on a symbolic computation system (Analytica). In 2009, he led the creation of the Computational Modeling and Analysis of Complex Systems (CMACS) center, funded by the 1850: 1865: 1885: 862: 431: 568: 1221: 638: 1820: 1810: 447: 629:
in 2008 in "recognition of his role in the invention of model checking and his sustained leadership in the area for more than two decades." In 2012, he
855: 1825: 1815: 622: 1713: 1214: 663: 57: 848: 599: 564: 521: 348: 767:
Bauer, Andrej; Clarke, Edmund; Zhao, Xudong (1998). "Analytica – An Experiment in Combining Theorem Proving and Symbolic Computation".
1835: 1285: 572: 1880: 458: 79: 1840: 1589: 965: 742: 520:
was also developed by his group. This important technique was the subject of Kenneth McMillan's Ph.D. thesis, which received an
1860: 1830: 1429: 1207: 816: 618: 1875: 743:"Edmund Clarke Pioneered Methods For Detecting Software, Hardware Errors | Carnegie Mellon School of Computer Science" 595: 1525: 801: 1855: 536: 477: 50: 44: 435: 336: 210: 621:
in 2005 for contributions to the formal verification of hardware and software correctness. He was elected to the
481: 379: 61: 532: 517: 439: 423: 840: 606: 540: 1453: 872: 602: 395: 375: 363: 128: 610: 509: 1069: 1187: 1805: 1800: 1183: 1143: 1073: 724: 501: 485: 399: 238: 997: 1681: 931: 682: 317: 266: 1637: 1481: 1357: 1293: 1277: 993: 947: 642: 529: 419: 407: 305: 256: 163: 1131: 1517: 1489: 973: 474: 320: 1709: 1693: 1661: 1617: 1329: 1321: 1107: 1017: 969: 927: 887: 776: 591: 583: 493: 427: 411: 403: 367: 340: 332: 251: 233: 200: 1769: 1725: 1701: 1569: 1553: 1477: 1437: 1409: 1349: 1301: 1261: 1179: 1117: 1037: 1027: 987: 977: 959: 883: 835: 580: 548: 415: 391: 720: 442:. He was appointed Full Professor in 1989. In 1995, he became the first recipient of the 414:
in 1976. After receiving his Ph.D., he taught in the Department of Computer Science at
103: 1753: 1689: 1673: 1645: 1629: 1621: 1549: 1469: 1393: 1253: 1165: 1059: 1023: 1011: 937: 909: 891: 651: 626: 613: 544: 513: 505: 497: 383: 344: 313: 173: 450:. He became a University Professor in 2008 and became an emeritus professor in 2015. 1794: 1777: 1761: 1737: 1721: 1665: 1605: 1445: 1421: 1417: 1401: 1373: 1269: 1173: 1161: 1135: 1125: 1101: 1055: 1043: 1033: 1005: 941: 919: 587: 261: 637:
for his outstanding contributions to the field of informatics. He received the 2014
434:. He left Harvard in 1982 to join the faculty in the Computer Science Department at 1741: 1461: 1389: 1381: 1317: 1309: 1230: 1169: 1121: 1085: 1079: 953: 895: 576: 539:. This center has a team of researchers, spanning multiple universities, applying 525: 443: 351: 328: 183: 151: 831: 1653: 1533: 1509: 1501: 1341: 1245: 1139: 1063: 1049: 1001: 983: 821: 489: 387: 371: 1199: 1749: 1729: 1597: 1565: 1561: 1541: 1365: 1333: 1157: 1153: 913: 903: 899: 780: 147: 1585: 1493: 1147: 1113: 1095: 1091: 797: 630: 17: 1846:
Harvard John A. Paulson School of Engineering and Applied Sciences faculty
1577: 1233: 721:"My father, Edmund M Clarke, passed away from Covid today. [...]" 647: 470: 454: 324: 309: 1891:
The Benjamin Franklin Medal in Computer and Cognitive Science laureates
811: 728: 694: 634: 223:
Completeness and Incompleteness Theorems for Hoare-Like Axiom Systems
560: 217: 528:
Award. In addition, his research group developed the first parallel
1203: 844: 806: 284: 29: 1871:
Members of the United States National Academy of Engineering
826: 1851:
1998 fellows of the Association for Computing Machinery
571:. He received a Technical Excellence Award from the 1866:
Fellows of the American Academy of Arts and Sciences
304:(July 27, 1945 – December 22, 2020) was an American 586:Department in 1999. He was a co-winner along with 279: 244: 232: 216: 206: 196: 179: 169: 159: 136: 110: 94: 1886:Deaths from the COVID-19 pandemic in Pennsylvania 639:Bower Award and Prize for Achievement in Science 1215: 856: 484:. In his Ph.D. thesis he proved that certain 8: 1222: 1208: 1200: 873:Paris Kanellakis Theory and Practice Award 863: 849: 841: 579:Award for Excellence in Research from the 504:. His research group pioneered the use of 448:Carnegie Mellon School of Computer Science 102: 91: 80:Learn how and when to remove this message 457:in December 2020, at age 75, during the 43:This article includes a list of general 807:Home page at Carnegie Mellon University 675: 446:Professorship, an endowed chair in the 426:where he was an assistant professor of 27:American computer scientist (1945–2020) 418:, for two years. In 1978, he moved to 719:James S. Clarke (22 December 2020). 623:American Academy of Arts and Sciences 488:control structures did not have good 7: 664:List of pioneers in computer science 492:. In 1981 he and his Ph.D. student 1821:Carnegie Mellon University faculty 1811:People from Newport News, Virginia 573:Semiconductor Research Corporation 49:it lacks sufficient corresponding 25: 459:COVID-19 pandemic in Pennsylvania 500:as a verification technique for 34: 812:Online biography from home page 619:National Academy of Engineering 605:in 1999 for the development of 502:finite-state concurrent systems 769:Journal of Automated Reasoning 631:received an honorary doctorate 1: 1826:University of Virginia alumni 802:Mathematics Genealogy Project 1816:American computer scientists 469:Clarke's interests included 432:Division of Applied Sciences 609:. In 2004 he received the 537:National Science Foundation 1907: 625:in 2011. He received the 496:first proposed the use of 436:Carnegie Mellon University 337:Carnegie Mellon University 211:Carnegie Mellon University 1836:Cornell University alumni 1240: 879: 817:Turing Award announcement 683:Edmund Melson Clarke, Jr. 490:Hoare-style proof systems 482:automatic theorem proving 302:Edmund Melson Clarke, Jr. 275: 189: 115:Edmund Melson Clarke, Jr. 101: 1881:Scientists from Virginia 834:publications indexed by 555:Professional recognition 518:binary decision diagrams 1841:Duke University faculty 781:10.1023/A:1006079212546 607:symbolic model checking 541:abstract interpretation 64:more precise citations. 1861:Turing Award laureates 1831:Duke University alumni 1254:Maurice Vincent Wilkes 603:Paris Kanellakis Award 376:University of Virginia 364:Newport News, Virginia 129:Newport News, Virginia 1876:Formal methods people 611:IEEE Computer Society 510:hardware verification 339:. Clarke, along with 312:noted for developing 486:programming language 366:, Clarke received a 347:, received the 2007 327:designs. He was the 239:Robert Lee Constable 1856:Fellows of the IEEE 1682:Michael Stonebraker 1454:Fernando J. Corbató 822:Model Checking book 267:Kenneth L. McMillan 1638:Charles P. Thacker 1482:Richard E. Stearns 1358:Kenneth E. Iverson 1294:Edsger W. Dijkstra 1278:James H. Wilkinson 1231:A. M. Turing Award 836:Microsoft Academic 695:"Edmund M. Clarke" 643:Franklin Institute 547:to biological and 420:Harvard University 408:Cornell University 318:formally verifying 306:computer scientist 257:Bhubaneswar Mishra 164:Cornell University 1788: 1787: 1646:Leslie G. Valiant 1518:Douglas Engelbart 1490:Edward Feigenbaum 1197: 1196: 398:, in 1968, and a 299: 298: 245:Doctoral students 191:Scientific career 184:A.M. Turing Award 140:December 22, 2020 90: 89: 82: 16:(Redirected from 1898: 1781: 1773: 1765: 1757: 1745: 1733: 1717: 1710:John L. Hennessy 1705: 1697: 1694:Whitfield Diffie 1685: 1677: 1669: 1662:Shafi Goldwasser 1657: 1649: 1641: 1633: 1625: 1618:E. Allen Emerson 1614:Edmund M. Clarke 1609: 1601: 1593: 1581: 1573: 1557: 1545: 1537: 1529: 1521: 1513: 1505: 1497: 1485: 1473: 1465: 1457: 1449: 1441: 1433: 1425: 1413: 1405: 1397: 1385: 1377: 1369: 1361: 1353: 1345: 1337: 1330:Michael O. Rabin 1325: 1322:Herbert A. Simon 1313: 1305: 1297: 1289: 1281: 1273: 1265: 1257: 1249: 1224: 1217: 1210: 1201: 865: 858: 851: 842: 832:Edmund M. Clarke 798:Edmund M. Clarke 785: 784: 764: 758: 757: 755: 753: 739: 733: 732: 716: 710: 709: 707: 705: 691: 685: 680: 596:Kenneth McMillan 592:E. Allen Emerson 584:Computer Science 549:embedded systems 494:E. Allen Emerson 428:Computer Science 404:Computer Science 341:E. Allen Emerson 333:Computer Science 295: 292: 290: 288: 286: 252:E. Allen Emerson 234:Doctoral advisor 228: 201:Computer science 143: 124: 122: 106: 96:Edmund M. Clarke 92: 85: 78: 74: 71: 65: 60:this article by 51:inline citations 38: 37: 30: 21: 1906: 1905: 1901: 1900: 1899: 1897: 1896: 1895: 1791: 1790: 1789: 1784: 1776: 1770:Robert Metcalfe 1768: 1760: 1748: 1736: 1726:Geoffrey Hinton 1720: 1714:David Patterson 1708: 1702:Tim Berners-Lee 1700: 1688: 1680: 1672: 1660: 1652: 1644: 1636: 1628: 1612: 1604: 1596: 1584: 1576: 1570:Leonard Adleman 1560: 1554:Kristen Nygaard 1548: 1540: 1532: 1524: 1516: 1508: 1500: 1488: 1478:Juris Hartmanis 1476: 1468: 1460: 1452: 1444: 1438:Ivan Sutherland 1436: 1428: 1416: 1408: 1400: 1388: 1380: 1372: 1364: 1356: 1350:Robert W. Floyd 1348: 1340: 1328: 1316: 1308: 1302:Charles Bachman 1300: 1292: 1284: 1276: 1268: 1262:Richard Hamming 1260: 1252: 1244: 1236: 1228: 1198: 1193: 875: 871:Winners of the 869: 827:CMACS home page 794: 789: 788: 766: 765: 761: 751: 749: 741: 740: 736: 718: 717: 713: 703: 701: 693: 692: 688: 681: 677: 672: 660: 581:Carnegie Mellon 575:in 1995 and an 557: 467: 416:Duke University 392:Duke University 380:Charlottesville 360: 316:, a method for 283: 271: 226: 160:Alma mater 155: 145: 141: 132: 126: 120: 118: 117: 116: 97: 86: 75: 69: 66: 56:Please help to 55: 39: 35: 28: 23: 22: 15: 12: 11: 5: 1904: 1902: 1894: 1893: 1888: 1883: 1878: 1873: 1868: 1863: 1858: 1853: 1848: 1843: 1838: 1833: 1828: 1823: 1818: 1813: 1808: 1803: 1793: 1792: 1786: 1785: 1783: 1782: 1774: 1766: 1758: 1754:Jeffrey Ullman 1746: 1734: 1718: 1706: 1698: 1690:Martin Hellman 1686: 1678: 1674:Leslie Lamport 1670: 1658: 1650: 1642: 1634: 1630:Barbara Liskov 1626: 1622:Joseph Sifakis 1610: 1602: 1594: 1582: 1574: 1558: 1550:Ole-Johan Dahl 1546: 1538: 1530: 1522: 1514: 1506: 1498: 1486: 1474: 1470:Butler Lampson 1466: 1458: 1450: 1442: 1434: 1426: 1414: 1406: 1398: 1394:Dennis Ritchie 1386: 1378: 1370: 1362: 1354: 1346: 1338: 1326: 1314: 1306: 1298: 1290: 1282: 1274: 1266: 1258: 1250: 1241: 1238: 1237: 1229: 1227: 1226: 1219: 1212: 1204: 1195: 1194: 1192: 1191: 1177: 1151: 1129: 1111: 1105: 1099: 1089: 1083: 1077: 1067: 1053: 1047: 1041: 1031: 1021: 1015: 1009: 991: 981: 963: 957: 951: 945: 935: 917: 907: 880: 877: 876: 870: 868: 867: 860: 853: 845: 839: 838: 829: 824: 819: 814: 809: 804: 793: 792:External links 790: 787: 786: 775:(3): 295–325. 759: 734: 727:) – via 711: 686: 674: 673: 671: 668: 667: 666: 659: 656: 652:Phi Beta Kappa 627:Herbrand Award 614:Harry H. Goode 556: 553: 545:model checking 533:theorem prover 514:model checking 506:model checking 498:model checking 466: 463: 440:Pittsburgh, PA 382:, in 1967, an 359: 356: 345:Joseph Sifakis 314:model checking 297: 296: 281: 277: 276: 273: 272: 270: 269: 264: 259: 254: 248: 246: 242: 241: 236: 230: 229: 220: 214: 213: 208: 204: 203: 198: 194: 193: 187: 186: 181: 177: 176: 174:Model checking 171: 170:Known for 167: 166: 161: 157: 156: 146: 144:(aged 75) 138: 134: 133: 127: 114: 112: 108: 107: 99: 98: 95: 88: 87: 42: 40: 33: 26: 24: 14: 13: 10: 9: 6: 4: 3: 2: 1903: 1892: 1889: 1887: 1884: 1882: 1879: 1877: 1874: 1872: 1869: 1867: 1864: 1862: 1859: 1857: 1854: 1852: 1849: 1847: 1844: 1842: 1839: 1837: 1834: 1832: 1829: 1827: 1824: 1822: 1819: 1817: 1814: 1812: 1809: 1807: 1804: 1802: 1799: 1798: 1796: 1779: 1778:Avi Wigderson 1775: 1771: 1767: 1763: 1762:Jack Dongarra 1759: 1755: 1751: 1747: 1743: 1739: 1735: 1731: 1727: 1723: 1722:Yoshua Bengio 1719: 1715: 1711: 1707: 1703: 1699: 1695: 1691: 1687: 1683: 1679: 1675: 1671: 1667: 1666:Silvio Micali 1663: 1659: 1655: 1651: 1647: 1643: 1639: 1635: 1631: 1627: 1623: 1619: 1615: 1611: 1607: 1606:Frances Allen 1603: 1599: 1595: 1591: 1587: 1583: 1579: 1575: 1571: 1567: 1563: 1559: 1555: 1551: 1547: 1543: 1539: 1535: 1531: 1527: 1523: 1519: 1515: 1511: 1507: 1503: 1499: 1495: 1491: 1487: 1483: 1479: 1475: 1471: 1467: 1463: 1459: 1455: 1451: 1447: 1446:William Kahan 1443: 1439: 1435: 1431: 1427: 1423: 1422:Robert Tarjan 1419: 1418:John Hopcroft 1415: 1411: 1407: 1403: 1402:Niklaus Wirth 1399: 1395: 1391: 1387: 1383: 1379: 1375: 1374:Edgar F. Codd 1371: 1367: 1363: 1359: 1355: 1351: 1347: 1343: 1339: 1335: 1331: 1327: 1323: 1319: 1315: 1311: 1307: 1303: 1299: 1295: 1291: 1287: 1286:John McCarthy 1283: 1279: 1275: 1271: 1270:Marvin Minsky 1267: 1263: 1259: 1255: 1251: 1247: 1243: 1242: 1239: 1235: 1232: 1225: 1220: 1218: 1213: 1211: 1206: 1205: 1202: 1189: 1185: 1181: 1178: 1175: 1171: 1167: 1163: 1159: 1155: 1152: 1149: 1145: 1141: 1137: 1133: 1130: 1127: 1123: 1119: 1115: 1112: 1109: 1106: 1103: 1100: 1097: 1093: 1090: 1087: 1084: 1081: 1078: 1075: 1071: 1068: 1065: 1061: 1057: 1054: 1051: 1048: 1045: 1042: 1039: 1035: 1032: 1029: 1025: 1022: 1019: 1016: 1013: 1010: 1007: 1003: 999: 995: 992: 989: 985: 982: 979: 975: 971: 967: 964: 961: 958: 955: 952: 949: 946: 943: 939: 936: 933: 929: 925: 921: 918: 915: 911: 908: 905: 901: 897: 893: 889: 885: 882: 881: 878: 874: 866: 861: 859: 854: 852: 847: 846: 843: 837: 833: 830: 828: 825: 823: 820: 818: 815: 813: 810: 808: 805: 803: 799: 796: 795: 791: 782: 778: 774: 770: 763: 760: 748: 744: 738: 735: 730: 726: 722: 715: 712: 700: 696: 690: 687: 684: 679: 676: 669: 665: 662: 661: 657: 655: 653: 649: 644: 640: 636: 632: 628: 624: 620: 615: 612: 608: 604: 601: 597: 593: 589: 588:Randal Bryant 585: 582: 578: 574: 570: 566: 562: 559:Clarke was a 554: 552: 550: 546: 542: 538: 534: 531: 527: 523: 519: 515: 511: 507: 503: 499: 495: 491: 487: 483: 479: 476: 472: 464: 462: 460: 456: 453:He died from 451: 449: 445: 441: 437: 433: 429: 425: 424:Cambridge, MA 421: 417: 413: 409: 405: 401: 397: 393: 389: 385: 381: 377: 373: 369: 365: 357: 355: 353: 350: 346: 342: 338: 334: 331:Professor of 330: 326: 322: 319: 315: 311: 307: 303: 294: 282: 278: 274: 268: 265: 263: 262:David L. Dill 260: 258: 255: 253: 250: 249: 247: 243: 240: 237: 235: 231: 224: 221: 219: 215: 212: 209: 205: 202: 199: 195: 192: 188: 185: 182: 178: 175: 172: 168: 165: 162: 158: 153: 149: 139: 135: 130: 125:July 27, 1945 113: 109: 105: 100: 93: 84: 81: 73: 70:February 2013 63: 59: 53: 52: 46: 41: 32: 31: 19: 1742:Pat Hanrahan 1613: 1462:Robin Milner 1410:Richard Karp 1390:Ken Thompson 1382:Stephen Cook 1318:Allen Newell 1310:Donald Knuth 1144:Mitzenmacher 923: 772: 768: 762: 750:. Retrieved 746: 737: 714: 702:. Retrieved 698: 689: 678: 577:Allen Newell 558: 526:Dissertation 478:verification 468: 452: 444:FORE Systems 361: 352:Turing Award 329:FORE Systems 301: 300: 222: 207:Institutions 190: 152:Pennsylvania 142:(2020-12-22) 76: 67: 48: 18:E. M. Clarke 1806:2020 deaths 1801:1945 births 1654:Judea Pearl 1534:Fred Brooks 1510:Amir Pnueli 1502:Manuel Blum 1342:John Backus 1246:Alan Perlis 752:24 December 704:24 December 512:. Symbolic 388:mathematics 372:mathematics 62:introducing 1795:Categories 1750:Alfred Aho 1738:Ed Catmull 1730:Yann LeCun 1598:Peter Naur 1566:Adi Shamir 1562:Ron Rivest 1542:Andrew Yao 1430:John Cocke 1366:Tony Hoare 1334:Dana Scott 1018:Buchberger 747:Cs.cmu.edu 699:Cs.cmu.edu 670:References 530:resolution 402:degree in 386:degree in 370:degree in 148:Pittsburgh 121:1945-07-27 45:references 1586:Vint Cerf 1494:Raj Reddy 1234:laureates 1184:Ferragina 1074:Leiserson 960:Franaszek 948:Karmarkar 641:from the 524:Doctoral 412:Ithaca NY 396:Durham NC 374:from the 358:Biography 1590:Bob Kahn 1578:Alan Kay 1526:Jim Gray 1166:McSherry 1060:Charikar 1044:Mehlhorn 994:Holzmann 988:Schapire 978:Strassen 932:McMillan 658:See also 648:Sigma Xi 567:and the 475:hardware 471:software 455:COVID-19 362:Born in 325:software 321:hardware 310:academic 1756:(2020) 1188:Manzini 1180:Burrows 1126:Szegedy 1118:Gibbons 1108:Pevzner 1102:Shenker 1070:Blumofe 1038:Rogaway 1034:Bellare 1012:Brayton 998:Kurshan 974:Solovay 938:Sleator 928:Emerson 892:Hellman 884:Adleman 800:at the 729:Twitter 635:TU Wien 598:of the 563:of the 430:in the 280:Website 58:improve 1780:(2023) 1772:(2022) 1764:(2021) 1744:(2019) 1732:(2018) 1716:(2017) 1704:(2016) 1696:(2015) 1684:(2014) 1676:(2013) 1668:(2012) 1656:(2011) 1648:(2010) 1640:(2009) 1632:(2008) 1624:(2007) 1608:(2006) 1600:(2005) 1592:(2004) 1580:(2003) 1572:(2002) 1556:(2001) 1544:(2000) 1536:(1999) 1528:(1998) 1520:(1997) 1512:(1996) 1504:(1995) 1496:(1994) 1484:(1993) 1472:(1992) 1464:(1991) 1456:(1990) 1448:(1989) 1440:(1988) 1432:(1987) 1424:(1986) 1412:(1985) 1404:(1984) 1396:(1983) 1384:(1982) 1376:(1981) 1368:(1980) 1360:(1979) 1352:(1978) 1344:(1977) 1336:(1976) 1324:(1975) 1312:(1974) 1304:(1973) 1296:(1972) 1288:(1971) 1280:(1970) 1272:(1969) 1264:(1968) 1256:(1967) 1248:(1966) 1190:(2022) 1176:(2021) 1170:Nissim 1150:(2020) 1140:Karlin 1136:Broder 1128:(2019) 1122:Matias 1110:(2018) 1104:(2017) 1098:(2016) 1088:(2015) 1082:(2014) 1080:Demmel 1076:(2013) 1066:(2012) 1056:Broder 1052:(2011) 1046:(2010) 1040:(2009) 1030:(2008) 1028:Vapnik 1024:Cortes 1020:(2007) 1014:(2006) 1008:(2005) 1006:Wolper 990:(2004) 984:Freund 980:(2003) 966:Miller 962:(2002) 956:(2001) 950:(2000) 944:(1999) 942:Tarjan 934:(1998) 924:Clarke 920:Bryant 916:(1997) 910:Lempel 906:(1996) 904:Shamir 900:Rivest 896:Merkle 888:Diffie 594:, and 561:fellow 516:using 227:(1976) 225:  218:Thesis 197:Fields 180:Awards 154:, U.S. 131:, U.S. 47:, but 1174:Smith 1162:Dwork 1158:Dinur 1148:Upfal 1064:Indyk 1050:Samet 1002:Vardi 970:Rabin 954:Myers 725:Tweet 633:from 406:from 400:Ph.D. 390:from 293:/~emc 1154:Blum 1132:Azar 1114:Alon 1096:Naor 1092:Fiat 1086:Luby 754:2020 706:2020 650:and 569:IEEE 543:and 508:for 480:and 473:and 465:Work 384:M.A. 368:B.A. 343:and 323:and 308:and 291:.edu 289:.cmu 137:Died 111:Born 914:Ziv 777:doi 600:ACM 565:ACM 522:ACM 349:ACM 335:at 287:.cs 285:www 1797:: 1752:; 1740:; 1728:; 1724:; 1712:; 1692:; 1664:; 1620:; 1616:; 1588:; 1568:; 1564:; 1552:; 1492:; 1480:; 1420:; 1392:; 1332:; 1320:; 1186:, 1182:, 1172:, 1168:, 1164:, 1160:, 1156:, 1146:, 1142:, 1138:, 1134:, 1124:, 1120:, 1116:, 1094:, 1072:, 1062:, 1058:, 1036:, 1026:, 1004:, 1000:, 996:, 986:, 976:, 972:, 968:, 940:, 930:, 926:, 922:, 912:, 902:, 898:, 894:, 890:, 886:, 773:21 771:. 745:. 697:. 654:. 590:, 551:. 461:. 438:, 422:, 410:, 394:, 378:, 354:. 150:, 1223:e 1216:t 1209:v 864:e 857:t 850:v 783:. 779:: 756:. 731:. 723:( 708:. 123:) 119:( 83:) 77:( 72:) 68:( 54:. 20:)

Index

E. M. Clarke
references
inline citations
improve
introducing
Learn how and when to remove this message

Newport News, Virginia
Pittsburgh
Pennsylvania
Cornell University
Model checking
A.M. Turing Award
Computer science
Carnegie Mellon University
Thesis
Doctoral advisor
Robert Lee Constable
E. Allen Emerson
Bhubaneswar Mishra
David L. Dill
Kenneth L. McMillan
www.cs.cmu.edu/~emc
computer scientist
academic
model checking
formally verifying
hardware
software
FORE Systems

Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.