Research Overview

My research interests are varied, although the common underlying thread over the past 20 years has been automated reasoning, also known as automated theorem proving. Over the last two 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, and the Cook-Levin theorem.

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.

Recently I have become interested in the potential of grid computing. My initial interest stemmed from the idea of using grid computing to find mechanical proofs of difficult theorems, and I am experimenting with a grid-enabled theorem prover. After delving into the technology I found myself interested in other applications of grid computing, and I have supervised some graduate students in such projects. With support from the NSF's Computational Science Training for Undergraduates in the Mathematical Sciences (CSUMS) program, Siguna Müller and I are developing a sequence of study and research activities in cryptography, resulting in the Wyoming Cryptography School (WCS). As part of the WCS, I am creating a course in grid computing for cryptographic applications, and I am currently supervising two Master's students whose research supports the WCS. In the long term, I hope to apply automated reasoning techniques to problems in cryptography inspired by the WCS.

My other current research interest in 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 is to develop tools that 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 will enable formal verification (via theorem proving) to be applied to more software. The WPW is an ambitious project, and its future success depends on whether enough students are interested in pursuing research in this area. Currently I have a Ph.D. student working on the WPW, as part of an NSF Science of Design project.