Formal verification is highly desirable in safety-critical applications such as embedded medical devices, spacecraft and aircraft control, as well as autonomous vehicles such as self-driving cars. The recipients invented a highly engineered tool that can be used to verify computing systems. It opens a broad range of software programs and hardware designs to formal verification, leading to safer and more secure software for a variety of uses. The award citation notes that the latest version of this formal methods tool, known as ACL2, is "the only simulation/verification system that provides a standard modeling language and industrial strength model simulation in a unified framework." Since the 1970's, Boyer, Moore, Kaufmann, and the users of their tools have continually redefined the state of the art of verification by verifying actual running code, demonstrating that theorem-proving technology has reached the stage where commercial-scale application is feasible. Robert S. Boyer is a professor in the Computer Sciences, Mathematics, and Philosophy Departments at the University of Texas at Austin. He was a Senior Computing Research Scientist at Computational Logic, Inc, and a Senior Member of Technical Staff at Microelectronics and Computer Technology Corp. He also was a research mathematician and staff scientist at SRI International. He graduated from the University of Texas at Austin with a B.A. in 1967, and he earned a Ph.D. in Mathematics from UT Austin in 1971. He is a Fellow of the American Association for Artificial Intelligence. J Strother Moore holds the Admiral B.R. Inman Centennial Chair in Computing Theory at the University of Texas at Austin, and is chair of the Department of Computer Sciences. He was a founder and chief scientist at Computational Logic, Inc. and served as its chief scientist for ten years. He was also a research mathematician at Xerox PARC and a staff scientist at SRI International. He earned an S.B. from the Massachusetts Institute of Technology in 1970, and a Ph.D. in Computational Logic from the University of Edinburgh in 1973. Moore is a Fellow of the American Association for Artificial Intelligence. Boyer and Moore were awarded the 1991 Current Prize in Automatic Theorem Proving by the American Mathematical Society. In 1999, they were awarded the Herbrand Award for their work in automatic theorem proving. Matt Kaufmann is a Senior Research Scientist at the University of Texas at Austin. Prior to joining the University, he worked with several technology firms, including Advanced Micro Devices, EDS, Motorola, Computational Logic, and Burroughs Corporation; before that, he was an assistant professor of Mathematics at Purdue University. Kaufmann earned an S.B. from the Massachusetts Institute of Technology in 1973, and a Ph.D. in Mathematics from the University of Wisconsin at Madison in 1978. Kaufmann has contributed to numerous professional journals and publications and has made substantial contributions to instructional, support and technology transfer activities. ACM will present the Software System Award to the honorees at the annual ACM Awards Banquet May 20, 2006, at the Westin St. Francis in San Francisco, Calif.