Mechanized Theorem Proving Research Group

Mechanized Theorem Proving Research Group

 ``When you have something that looks like a good idea, give it your best shot''
-- Woody Bledsoe, 1921--1995

``The reason so many deep theorems are proved with the Boyer-Moore theorem prover is that only smart people use it!''
-- anonymous critic

Can we build machines that reason? Yes! UT Austin has a long tradition of building such machines, going back to the pioneering work of Woody Bledsoe (photo above) from the 1960's onwards.

Our research group is the home of some of the most powerful automatic theorem proving engines in the world, including ACL2 and its predecessor, the Boyer-Moore theorem prover Nqthm. The authors of this software (Bob Boyer, J Moore, and Matt Kaufmann; see below) won the 2005 ACM Software System Award, awarded for software systems that have had lasting influence, ``reflected in contributions to concepts, in commercial acceptance, or both.''

The faculty members in automatic theorem proving research at UT are Bob Boyer (now retired but Emeritus), Warren A. Hunt, Jr., and J Moore. As a co-author of ACL2 and a long-time contributor to the Boyer-Moore project, Matt Kaufmann is a research staff member who is also an active member of the group. For more information see our home pages (Boyer, Hunt, Moore, Kaufmann), or contact one of us by email (last name cs utexas edu, with an at-sign and dots in the obvious places).

We meet regularly to discuss current issues in automatic theorem proving. These days our meetings largely concern ongoing ACL2 projects or connections between ACL2 and other theorem proving methodologies. Our seminar schedule is posted online (including past meetings) and those interested in automated reasoning are welcome to attend.

For a little more information about what we do, read on. Two books about ACL2 describe our work in more detail. See especially Overview (.8 MB postscript file) of the first book.

What Have We Proved?

Among the many theorems proved with UT theorem provers are the following: Clearly, our theorem provers touch upon and often raise deep and interesting questions in mathematics, logic and artificial intelligence.

But our theorem provers are not just of academic interest. A specialty of our theorem provers is the correctness of ``digital artifacts,'' i.e., hardware designs, instruction set architectures, microarchitecture models, and software. UT theorem provers have been used to prove the correctness of

Many of the proofs above were undertaken by researchers working for the companies named. The proofs often uncovered bugs in well-tested designs -- bugs that were fixed before fabrication.

Thus, our theorem provers are valuable industrial tools. Mechanical theorem proving may be industry's best hope for coping with the complexity of modern designs -- and industry knows it! The industry today seeks people with the skills to use and develop these tools.

A Thumbnail History

Bledsoe is largely responsible for establishing a theorem proving tradition at UT. But others have had important roles, perhaps none more so than Don Good, who with J.C. Browne and Bledsoe established and led the Institute for Computing Science and Computer Applications (ICSCA). ICSCA was located in the 20th and 21st floors of the UT Tower. In the 1970's and early 80's, the major research thrust of ICSCA was program verification. Good and his colleagues developed one of the earliest successful program verification systems, named Gypsy. The theorem prover in the Gypsy verification system was initially based on the prover developed by Bledsoe in the mid-70's. While the Gypsy prover evolved a lot, its relationship to the Bledsoe provers was always clear.

In 1981, Boyer and Moore joined the CS faculty at UT and also joined ICSCA. Their Nqthm theorem prover became a second main thrust at ICSCA.

In 1983, Good, Rich Cohen, Boyer, Moore, and Mike Smith founded Computational Logic, Inc. (CLI). The goal of the corporation was to move verification technology to industry and to continue formal methods research. For several years CLI existed only on paper; the principals performed private consulting and donated part of the revenue to the company. In 1987, CLI acquired offices off campus and within a few years the entire ICSCA operation had moved to CLI, under the leadership of Don Good, who was both President and Chairman of the Board. The company, still oriented toward transfer of verification technology to industry, did not sell a product but performed contract research for government and industry. Ownership in the company was distributed among the employees. Boyer remained a UT professor; Moore was an adjunct professor and taught several courses while at CLI, including one (on machine-code verification) on the CLI premises. Many PhDs were awarded to students who were working at CLI.

In 1999, CLI officially closed its doors and distributed its assets to the shareholders. Many ex-CLI employees are now working in formal methods in industry.

Many of the fundamental advances in theorem proving made by the UT Mechanized Theorem Proving research group actually occurred as contract research conducted at CLI. (For example, the Motorola CAP DSP verification and the AMD K5 floating-point division proof were CLI projects.)

In addition to the theorem provers of Bledsoe, Boyer, Moore and Kaufmann, a number of other systems have been created by members of our group, including a remarkable geometry theorem prover by Shang-ching Chou, PVS by Natarajan Shankar and others, the Lego system for constructive type theory by Randy Pollack, and a variant of ACL2 supporting non-standard analysis by Ruben Gamboa (see the documentation topic real in the ACL2 User's Manual).

People

Here are some of the people who have been in this research group in some capacity. This list includes several people who have made fundamental contributions to theorem proving and formal methods. Some members were students here. Some students completed Masters or PhDs at UT; others went elsewhere and sometimes completed their degrees there. Some members were post-docs, long-term visitors, research scientists or engineers in our group at the University of Texas at Austin, or employees of Computational Logic, Inc. The list is offered as evidence of the long life and activity of the group, not merely as a list of graduated students. The list is in roughly reverse chronological order. It does not include all of the professionals using ACL2 in industry, some of whom have made deeply significant contributions to the tool and the ACL2 community.