Knowledge

Edmund M. Clarke

Source 📝

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

Index

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
Computer Science

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