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, 19211995
``The reason so many deep theorems are proved with the BoyerMoore 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 BoyerMoore 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 coauthor of ACL2 and a longtime contributor to the BoyerMoore
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 atsign 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:
 the limit of a sum is the sum of the limits,
 the BolzanoWeierstrass Theorem,
 the Fundamental Theorem of calculus,
 Euler's identity,
 Gauss' law of quadratic reciprocity,
 the undecidability of the halting problem, and
 Godel's incompleteness theorem.
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
 the gatelevel design of an academic microprocessor  which was
then fabricated and tested,
 a compiler, an assembler, a linker, and a loader for the above
microprocessor,
 application programs written in the source language of the above
compiler
 the ``CLI stack''  the chaining together of the above theorems to
establish correctness of applications running on a fabricated chip,
 21 of the 22 routines in the Berkeley C String library (when compiled
by
gcc o
for the Motorola 68020),
 microcode programs extracted from the ROM of the Motorola CAP digital
signal processor,
 the microcode for floatingpoint division and square root on the AMD K5,
 the RTL implementing each of the elementary floatingpoint operations
on the AMD Athlon,
 safetycritical code involved in trainborne control software written
by Union Switch and Signal,
 components of the RockwellCollins Avionics JEM1, the world's first
Java virtual machine in silicon,
 bootstrapping code for the IBM 4758 secure coprocessor,
 class loader and bytecode verifier for the Sun Java Virtual Machine
 process separation on the RockwellCollins AAMP7G cryptoprocessor, allowing
the processor to obtain Multiple Independent Levels of Security (MILS) certification using
formal methods techniques as specified by EAL7 of the Common Criteria
Many of the proofs above were undertaken by researchers working for the
companies named. The proofs often uncovered bugs in welltested 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 mid70'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 machinecode 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 exCLI 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 floatingpoint 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 Shangching Chou,
PVS by Natarajan Shankar and others,
the Lego system for
constructive type theory by
Randy Pollack, and a variant of ACL2 supporting nonstandard 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
postdocs, longterm 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.
 Shilpi Goel
 Oswaldo Olivo
 Alan Dunn
 Nathan Wetzler
 Jared Davis
 Sol Swords
 John Erickson
 Ian Wehrman
 David Rager
 Qiang Zhang
 Sandip Ray
 Carlos Pacheco
 Michael N. Bogomolny
 Robert Krug
 Rob Sumners
 Pete Manolios
 Jun Sawada
 Ruben Antonio Gamboa
 Benjamin Price Shults
 Ken Albin
 John Cowles
 Matthew Michael Wilding
 Sakthikumar Subramanian
 Nicholas Freitag McPhee
 Yuan Yu
 Arthur David Flatau
 Jimi Crawford
 David Moshe Goldschlag
 Randy Pollack
 James Daniel Christian
 William R. Bevier
 William D. Young
 Ann Siebert
 Judy Crow
 Anand Tripathi
 Ben DiVito
 John McHugh
 Guohui Feng
 David Plummer
 Don Simon
 Larry Hines
 Miren Carranza
 Tie Cheng Wang
 Myung Won Kim
 Michael Vose
 Matt Kaufmann
 David Russinoff
 Natarajan Shankar
 Warren Alva Hunt, Jr.
 ShangChing Chou
 Mabry Tyson
 Dwight Hare
 Wilhelm Burger
 Charlie Hoch
 Larry Hunter
 Jim Williams
 Robert L. (Larry) Akers
 Larry Smith
 Mike Smith
 Rich Cohen
 John T Minor
 Peter Bruell
 Mark Steven Moriconi
 Vesko Genov Marinov
 J Strother Moore
 Donald I. Good
 Dallas Lankford
 Mike Ballantyne
 Robert S. Boyer
 Robert Anderson
 Charles Wilks
 James Morris
 Stephen Charles Darden
 Morris C Enfield
 John Ulrich
 James Hall
 Claude Duplissey
 Hugh Williamson