Kenneth L. McMillan is an American computer scientist working in the area of formal methods, logic, and programming languages. He is a professor in the computer science department at the University of Texas at Austin, where he holds the Admiral B.R. Inman Centennial Chair in Computing Theory. [1]
McMillan received his Ph.D. from Carnegie Mellon University in 1992, under Edmund M. Clarke. [2] He is credited to have invented symbolic model checking during his thesis work, which won him the 1992 ACM Doctoral Dissertation Award, the highest doctoral dissertation prize awarded by the Association for Computing Machinery (ACM). [3] He also won the 1998 ACM Paris Kanellakis Award for Theory and Practice jointly with Randal Bryant, Edmund Clarke, and E. Allen Emerson for work on symbolic model checking. [4] McMillan subsequently worked at Bell Labs, Cadence Berkeley Labs, and was a Principal Researcher at Microsoft Research, Redmond [5] before joining the faculty of University of Texas at Austin in 2021. [6]
McMillan pioneered several influential research areas in formal methods. His initial work on symbolic model checking based on binary decision diagrams culminated in the creation of the SMV/nuSMV family of model checkers. [7] He also pioneered techniques based on Craig interpolation in model checking infinite-state systems. [8] He is also known for his work on Constrained Horn Clause (CHC) solving [9] and the IVy distributed system verification tool. [10]
McMillan currently serves on the steering committee of the International Conference on Computer-Aided Verification (CAV). [16]
The Association for Computing Machinery (ACM) is a US-based international learned society for computing. It was founded in 1947 and is the world's largest scientific and educational computing society. The ACM is a non-profit professional membership group, reporting nearly 110,000 student and professional members as of 2022. Its headquarters are in New York City.
SIGPLAN is the Association for Computing Machinery's Special Interest Group on programming languages.
John Charles Reynolds was an American computer scientist.
The Paris Kanellakis Theory and Practice Award is granted yearly by the Association for Computing Machinery (ACM) to honor "specific theoretical accomplishments that have had a significant and demonstrable effect on the practice of computing". It was instituted in 1996, in memory of Paris C. Kanellakis, a computer scientist who died with his immediate family in an airplane crash in South America in 1995. The award is accompanied by a prize of $10,000 and is endowed by contributions from Kanellakis's parents, with additional financial support provided by four ACM Special Interest Groups, the ACM SIG Projects Fund, and individual contributions.
ACM SIGACT or SIGACT is the Association for Computing Machinery Special Interest Group on Algorithms and Computation Theory, whose purpose is support of research in theoretical computer science. It was founded in 1968 by Patrick C. Fischer.
The ACM–IEEE Symposium on Logic in Computer Science (LICS) is an annual academic conference on the theory and practice of computer science in relation to mathematical logic. Extended versions of selected papers of each year's conference appear in renowned international journals such as Logical Methods in Computer Science and ACM Transactions on Computational Logic.
The annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) is an academic conference in the field of computer science, with focus on fundamental principles in the design, definition, analysis, and implementation of programming languages, programming systems, and programming interfaces. The venue is jointly sponsored by two Special Interest Groups of the Association for Computing Machinery: SIGPLAN and SIGACT.
Rajeev Alur is an American professor of computer science at the University of Pennsylvania who has made contributions to formal methods, programming languages, and automata theory, including notably the introduction of timed automata and nested words.
Edmund Melson Clarke, Jr. was an American computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs. He was the FORE Systems Professor of Computer Science at Carnegie Mellon University. Clarke, along with E. Allen Emerson and Joseph Sifakis, received the 2007 ACM Turing Award.
Ernest Allen Emerson II, better known as E. Allen Emerson, is an American computer scientist and winner of the 2007 Turing Award. He is Professor and Regents Chair Emeritus at the University of Texas at Austin, United States.
Dexter Campbell Kozen is an American theoretical computer scientist. He is Joseph Newton Pew, Jr. Professor in Engineering at Cornell University. He received his B.A. from Dartmouth College in 1974 and his PhD in computer science in 1977 from Cornell University, where he was advised by Juris Hartmanis. He advised numerous Ph.D. students.
ISP is a tool for the formal verification of MPI programs developed within the School of Computing at the University of Utah. Like model checkers, such as SPIN, ISP verifies the complete state space of a system for a set of safety properties. However, unlike model checkers, ISP performs code level verification. This means that the tool verifies all relevant interleavings of a concurrent program by replaying the actual program code without building verification models. This idea was pioneered in a number of tools, notably by Godefroid, in his VeriSoft tool. Other recent tools of this genre include the Java Pathfinder, Microsoft's CHESS tool, and MODIST. Relevant interleavings are computed using a customized dynamic partial order reduction algorithm called POE.
George Ciprian Necula is a Romanian computer scientist, engineer at Google, and former professor at the University of California, Berkeley who does research in the area of programming languages and software engineering, with a particular focus on software verification and formal methods. He is best known for his Ph.D. thesis work first describing proof-carrying code, a work that received the 2007 SIGPLAN Most Influential POPL Paper Award.
Peter William O'Hearn, formerly a research scientist at Meta, is a Distinguished Engineer at Lacework and a Professor of Computer science at University College London (UCL). He has made significant contributions to formal methods for program correctness. In recent years these advances have been employed in developing industrial software tools that conduct automated analysis of large industrial codebases.
Kathryn S. McKinley is an American computer scientist noted for her research on compilers, runtime systems, and computer architecture. She is also known for her leadership in broadening participation in computing. McKinley was co-chair of CRA-W from 2011 to 2014.
ACM SIGOPS is the Association for Computing Machinery's Special Interest Group on Operating Systems, an international community of students, faculty, researchers, and practitioners associated with research and development related to operating systems. The organization sponsors international conferences related to computer systems, operating systems, computer architectures, distributed computing, and virtual environments. In addition, the organization offers multiple awards recognizing outstanding participants in the field, including the Dennis M. Ritchie Doctoral Dissertation Award, in honor of Dennis Ritchie, co-creator of the C programming language and Unix operating system.
David Lansing Dill is a computer scientist and academic noted for contributions to formal verification, electronic voting security, and computational systems biology.
Alessio Lomuscio is a professor of Safe Artificial Intelligence at the Department of Computing at Imperial College London. His research focuses on the verification of autonomous systems, specifically on providing formal safety guarantees for both Multi-agent systems as well as Machine Learning-enabled systems.
{{cite web}}: Missing or empty |title= (help){{cite web}}: Missing or empty |title= (help){{cite web}}: Missing or empty |title= (help)