Research Overview

My research interests are varied, although the common underlying thread over the past 30 years has been automated reasoning, also known as automated theorem proving. Over the last three decades, I have done research (some published, some not) in the fields of approximation algorithms, computer graphics, databases, automated reasoning, grid computing, and software engineering. The truth is that I find a lot of computer science problems to be very interesting, and I am willing to research any problem that sparks my curiosity.

For my Ph.D., I worked under the direction of Bob Boyer. As part of my dissertation I modified the theorem prover ACL2 to support the irrational numbers. The modified version is called ACL2(r) to avoid confusion with its more famous ancestor. Because ACL2 is an inductive theorem prover with little support for quantifiers or sets, the logical foundation of non-standard analysis provides a natural way to reason about the irrationals.

Formalizing theorems in ACL2 and ACL2(r) is another of my research interests. I have formalized many theorems about real analysis in ACL2(r), such as basic properties of common transcendental functions, Euler’s Formula, and Taylor’s Theorem. I have also done other formalizations in ACL2, including the correctness of a synthesized Kalman Filter implementation, Misra’s powerlists, red-black trees, the Cook-Levin theorem, the existence of transcendental numbers, and the correctness of approximation algorithms to transcendental functions.

I am currently seeking help with projects involving writing theorem provers and formalizing theorems in ACL2(r). If you are interested, check out my Help Wanted! page for some ideas.

In the recent past, I was also interested in the potential of grid computing, although I am no longer doing research in this area. My initial interest stemmed from the idea of using grid computing to find mechanical proofs of difficult theorems, but I later became more interested in using grid computing for scientific computation. With support from the NSF’s Computational Science Training for Undergraduates in the Mathematical Sciences (CSUMS) program, Siguna Müller and I developed a sequence of study and research activities in cryptography, resulting in the Wyoming Cryptography School (WCS). As part of the WCS, I created a course in grid computing for cryptographic applications, and I supervised two Master’s students whose research supports the WCS.

Another previous research interest was the Wyoming Programmer’s Workbench (WPW), an Eclipse-based environment that connects programs, unit test cases, and models. Professional programmers routinely deal with these three different types of artifacts. The goal of the WPW was to develop tools to make it easier for programmers to move from one artifact to another, e.g., by generating a model from a program and its test cases, or by generating test cases from a program and its model, or by generating a program directly from its model. These models are the formal artifacts that we use when reasoning about the program with an automated theorem prover, so the WPW would have enabled formal verification (via theorem proving) to be applied to more software. The WPW was an ambitious project, and its future depended on finding and funding enough students interested in pursuing research in this area. I graduated a Ph.D. student who worked on aspects of the WPW, as part of an NSF Science of Design project.

Leave a Reply