Potential Student Research @ Union College

The following are a series of projects/project ideas that I'm proposing. If any of them sound interesting to you and you have the time to work on it, reach out to me and we can discuss options. Possible avenues to work with me are Summer research, a work study, a research practicum, or an independent study. It all depends on how much time you have, your enthusiasm, and your ability to learn.

Proof Automation in an Interactive Thoerem Prover

High-Level Description of Components

I’m working on a large-scale development used to prove properties about programs. A component of this development is coded in OCaml. This is a work in progress, and has multiple sub-projecs that you can work on. You don’t need to understand the high-level goal of the entire project to be able to do useful tasks but here it is anyway.

Proofs in ITPs are harder to perform than proofs in ATPs but they are more desired, essentially because ATPs are more susceptible to bugs. The tool that I’m working on - SMTCoq - uses proofs from SMT solvers (a kind of ATP), to automate proofs in Coq (the ITP), making it easier to perform proofs in Coq. Since SMT solvers are more susceptible to bugs than Coq, the solver emits, in addition to its result, a certificate of its result. SMTCoq checks the SMT solver certificate to make sure that the result of the SMT solver is not buggy.

Project Task

A significant part of the SMTCoq codebase is a checker for proof certificates from SMT solvers. This checker has already been implemented for a particular language of proofs emitted by SMT solvers (let’s call this language L1 for convenience). Modern SMT solvers now produce proof certificates in a different language (L2). The high-level goal of this project is a translator from L2 down to L1. This translator will allow SMTCoq to support modern SMT solvers, without having to change the code for its checker. Changing the checker is a very difficult task. On the contrary, language translation is a relatively simple task. If you have taken CSC 370 in Fall 2024 with me, you will be familiar with language translation in OCaml. We built interpreters for functional and imperative programming languages that compiled the source code down to OCaml and evaluated them in OCaml. In this project, we interpret/translate L2 down to L1 so that we can utilize the infrastructure that already exists for proof certificates in L1.

Getting Involved

A large part of the translator is already built. You can find the code here. There are a lot of lines of code but fundamentally the structure of the program is pretty similar to interpreters written in CSC 370. Proofs are parsed down to a abstract syntax tree (AST) which is defined in the beginning of the linked file. The rest of the file defines functions that modify proof trees (instances of the AST). Tasks/possible projects:

The translator implementation does not handle many corner cases and you can help complete this implementation.
The translator needs to be exensively tested. We have a large set of benchmarks called SMTLib over which we need to test this tool. This task will involve setting up a large scale test suite on a server, aggregating results, but also modifying the OCaml parser so that it accepts certain kinds of inputs from the test files that are currently unaccepted
The debugging infrastructure for the checker is currently very poor. When the checker runs on a proof file, it succeeds or simply fails. We need to extract more fine-grained information especially in the case of failure from the checker so that we can locate the source of failure and fix it. This will entail writing some sort of Python script that can for the kind of low-level data that the checker is able to output, and translating that to some form of human-readable output. Such a debugging script also currently exists, but can use a lot of improvement. See this Github repo.

Possible next steps if you're interested:

I don't expect any of this to be fully clear to you from this text. As a first step, ask me specific follow up questions from the text. I can try and unpack some of the concepts, I can also point you to readings.
Some of the tools mentioned here will be discussed in more detail in the CSC 483. Taking that class is a natural next step if you’re interested in this line of research and want a more comprehensive understanding of the work.

Skills you will need:

Experience with OCaml or some other functional programming language. Ideally, you have taken CSC 370. For the Python script task, you don't need any OCaml skills but some efficiency with handling and manipulating non-trivial data in Python.
An ability to separate and reason about parts of a larger project while abstracting away details of the rest of the project.
Enthusiasm to learn, and work hard.

Things that you can potentially get out of this experience:

Money/credit depending on whether you choose to do a practicum, independent study, work-study, or Summer research.
Experience working with state-of-the-art software verification tools. This sort of experience is very valuable. Such experience is more and more sought after in industry and academia.
Experience developing within a large-scale software development.
This is a stretch goal, but depending on how involved you get in this project, you could be part of a research publication (this will most likely not occur if you only do 1 term of work on the project).

Mechanized Proofs in an Interactive Theorem Prover

This is one of the more challenging projects. There will be a lot of learning and hard work involved on your own, but it will be supervised by me. The learning curve is steep, but the work can be highly rewarding. Being able to do mechanized proofs is a niche and useful skill. whether you're going into academia or industry.

High-Level Description of Components

Coq is an interactive theorem prover (ITP), a software tool used to prove logical properties. It’s often used to prove properties about software. Properties in Coq are tedious and often difficult to prove, because it has limited supported for automation of proofs. However, ITP proofs are highly sought after in industry especially for safety-critical software systems - software whose failure could result in human fatality. For example, in airplanes, medical devices, weapon systems, etc. Another popular application of ITP proofs is in hardware verification - companies like Intel and Apple formally verify their hardware before they build them. Verification of hardware is done at the bit level. Since the verification of the hardware is done in software (recall that an ITP is a software tool), we need a theory to represent bits and proofs in this theory. Bit-vectors - arrays of bits - are commonly used to do bit-level specification and verification. I have been contributing to a bit-vector library in the Coq theorem prover. The library includes a representation of bit-vectors in Coq and proofs of many interesting properties over bit-vectors. The goal of this project is to make interesting contributions to this bit-vector library.

This is one of the more challenging projects but could be equally rewarding.

Skills you will need:

I don't expect you to have any experience with interactive theorem provers. You will need need to be driven and have the enthusiasm to learn.
You will spend some time learning theorem proving in ITPs on your own. This online book called Software Foundations offers an introduction to interactive theorem proving in Coq that is popular among the community, so its a good start (although you won't need to go all the way through to the end).
Once you get hang of the foundations, you will have to understand the current status of the proof library before you can start contributing. You can find the library here.