I am a PhD student at the University of Iowa, working with Prof. Cesare
Tinelli. I completed my Master's in Computer Science at
the University of Iowa, in Spring 2017. My research interests
lie in bridging the gap between SMT (satisfiability modulo
theories) solvers and proof assistants to get the most out of
the former's speed and the latter's reliability. Currently, I'm
exploring using abductive reasoning to make proofs interactive.
I have contributed to CVC4 (now cvc5),
and Kind2, the
model checker. More recently, I have been making contributions
to SMTCoq,
the Coq plugin that supports automation using SMT solvers.
I also enjoy teaching, particularly undergraduate computer
science courses.
I am from South India, and graduated from MVJ College of
Engineering at Bangalore, in 2015.
Department of Computer Science
1420 Seamans Center
University of Iowa
Iowa City, IA 52242-1419
USA
arjun-viswanathan @ uiowa.edu
Fall 2015 - Teaching Assistant, Introduction to Computer
Science
Fall 2016 - Teaching Assistant, Algorithms
Spring 2017 - Teaching Assistant, Programming Language
Concepts
Fall 2018 - Teaching Assistant, Formal Methods in Software
Engineering
Summer 2020 - Bedrock Systems, Formal Methods Group
Summer 2021 - GE Research
Spring 2022 - Visited Prof. Chantal Keller at the Formal
Methods Lab (Laboratoire Méthodes Formelles) in University
Paris-Saclay
Summer 2022 - Galois Inc.
Summer 2023 - Visited Prof. Haniel Barbosa at Federal
University of Minas Gerais (UFMG) in Belo Horizonte, Brazil
Datatypes with Shared Selectors
Andrew Reynolds, Arjun Viswanathan, Haniel Barbosa, Cesare
Tinelli, and Clark Barrett.
International Joint Conference on Automated Reasoning (IJCAR) 2018
Comparison of Proof Producing Systems
in SMT Solvers
Arjun Viswanathan.
Report presented as part of Qualifying Exam on 09/18/2018
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.
This series of reports were presented as part of my
comprehensive exam. They are an attempt at understanding how
SMTCoq works and comparing
it with the SMT integration in Isabelle/HOL. The last 3 were a
follow-up to the first one and I find them more instructive:
1. Automating
Interactive Theorem Provers and Certifying Automatic Theorem
Provers
2. Foundations
of Theorem Provers
3. Relating
Higher Order and First-Order Logics
4. Proof
Generation
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
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
Beyond
Model Checking of Idealized Lustre in Kind 2
Daniel Larraz, Arjun Viswanathan, Mickaël Laurent, Cesare Tinelli.
High Integrity Language Technology 2022
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
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
Comparison of Proof Producing Systems in SMT Solvers
Report presented as part of Qualifying Exam on 09/18/2018.
Verifying
Bit-vector Invertibility Conditions in Coq (Extended Abstract)
Presented at Proof eXchange for Theorem Proving (PxTP) 2019
Also presented as a short report and a 2 minute talk at the FMCAD
Student Forum 2019
Extending
SMTCoq with Abductive Reasoning
Presented at the Deducteam Seminar at the Formal Methods Lab
(Laboratoire Méthodes Formelles), University Paris-Saclay in
April, 2022
Abductive
Reasoning with SMT Solvers
Presented at the CS Graduate Symposium at the University of Iowa
in November, 2022
An
Interactive SMT Tactic in Coq using Abductive Reasoning
Presented at the International Conference on Logic for
Programming, Artificial Intelligence and Reasoning (LPAR) 2023