Student Research @ Union College

Potential Projects

Project 1: 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 the OCaml programming language. This is a work in progress, and has multiple sub-projecs that you can work on. The following is the high-level goal of the project.

Rocq 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 Rocq are tedious and often difficult to prove, because it has limited supported for automation of proofs. There also exist automated theorem provers (ATP), software tools that can prove logical properties automatically. A subset of these tools are called SMT (satisfiability modulo theories) solvers.

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 Rocq (the ITP), making it easier to perform proofs in Rocq. Since SMT solvers are more susceptible to bugs than Rocq, 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 CSC370, 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 CSC370. Proofs are parsed down to an 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 can be improved in many ways. For example, many functions have to be made tail-recursive.
• There are many corner cases that the translator does not currently work for. It needs to be fixed so that it is able to handle these. This task will involve being able to debug and improve a large OCaml project.
• The translator needs to be exensively tested. We have a large set of benchmarks called SMTLIB over which we need to test this tool. A former student has already run this set of benchmarks on a computing cluster. The success rate of the checker is low. It's success rate needs to be improved. This will entail debugging and fixing issues in the checker and rerunning the experiments on the cluster.

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.
• At the very least, you will need experience with building interpreters using functional programming languages. You will have to take CSC370 with me and do well in it. This will be offerred next in Winter 2027.

Skills you will need:

• Experience with OCaml or some other functional programming language. Ideally, you have taken CSC370.
• 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).

Project 2: Mechanized Proofs in an Interactive Theorem Prover

High-Level Description of Components

Rocq 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 Rocq 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 Rocq theorem prover. The library includes a representation of bit-vectors in Rocq and proofs of many interesting properties over bit-vectors. The goal of this project is to make interesting contributions to this bit-vector library.

Skills you will need:

• An understanding of the basics of bit-level operations in a computer. An understanding of the relationship between binary and decimal numbers. Having taken CSC270 (Computer Organization) will help.
• 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.

Past Projects

Polina Kozyarchuk

Ishaan Kumar

Ha Truong

Jacob Schuckman

Liam Secrist, Jordin Palmeri