Visiting Assistant Professor
Computer Science Department
Union College
Email: viswanaa @ union.edu
Office: 229 Steinmetz Hall
I'm from Hyderabad in South India. I studied Computer Engineering as an undergraduate at MVJ College of Engineering in Bangalore. Until August 2024, I was a Doctoral candidate advised by Prof. Cesare Tinelli at the University of Iowa, which is also where I have a Master's in computer science from.
Generally, my research interests lie in using formal methods tools to make software safer. My specific interests currently are in the integration of interactive theorem provers such as Coq with SMT solvers for solver reliability and proof automation.
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.
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. 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 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.
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 large 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.
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.
If you want to get more directly involved, write to me or come to my office hours. Possible avenues to work with me on this project 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.
Skills you will need:
Things that you can potentially get out of this experience:
Automating Interactive Theorem Provers and Certifying Automated Theorem
Provers
Arjun Viswanathan.
PhD Thesis, Fall 2024
Formal Verification of Bit-vector Invertibility Conditions in Coq
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark Barrett.
International Symposium on Frontiers of Combining Systems (FroCoS) 2023
An Interactive SMT Tactic in Coq using Abductive Reasoning
Haniel Barbosa, Chantal Keller, Andrew Reynolds, Arjun Viswanathan, Cesare Tinelli, Clark Barrett.
International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR) 2023
Beyond Model Checking of Idealized Lustre in Kind 2
Daniel Larraz, Arjun Viswanathan, Mickaël Laurent, Cesare Tinelli.
High Integrity Language Technology 2022
Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT
Baoluo Meng, Arjun Viswanathan, William Smith, Abha Moitra, Kit Siu, Michael Durling.
NASA Formal Methods 2022
Flexible Proof Production in an Industrial-Strength SMT Solver
Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias
Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark Barrett.
International Joint Conference on Automated Reasoning 2022
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark Barrett, Cesare Tinelli.
Proof eXchange for Theorem Proving (PxTP) 2019
- was awarded the Woody Bledsoe Award for student contributions.
Datatypes with Shared Selectors
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare Tinelli, and Clark Barrett.
International Joint Conference on Automated Reasoning (IJCAR) 2018