Datatypes with Shared Selectors. - Andrew Reynolds 001; Arjun Viswanathan 001; Haniel Barbosa; Cesare Tinelli; Clark W. Barrett (IJCAR, 2018)

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). - Burak Ekici; Arjun Viswanathan 001; Yoni Zohar; Clark W. Barrett; Cesare Tinelli (PxTP, 2019)

Flexible Proof Production in an Industrial-Strength SMT Solver. - Haniel Barbosa; Andrew Reynolds 001; Gereon Kremer; Hanna Lachnitt; Aina Niemetz; Andres Nötzli; Alex Ozdemir; Mathias Preiner; Arjun Viswanathan 001; Scott Viteri; Yoni Zohar; Cesare Tinelli; et al. (IJCAR, 2022)

Synthesis of Optimal Defenses for System Architecture Design Model in MaxSMT. - Baoluo Meng; Arjun Viswanathan 001; William Smith; Abha Moitra; Kit Siu; Michael Durling (NFM, 2022)

Formal Verification of Bit-Vector Invertibility Conditions in Coq. - Burak Ekici; Arjun Viswanathan 001; Yoni Zohar; Cesare Tinelli; Clark W. Barrett (FroCoS, 2023)

An Interactive SMT Tactic in Coq using Abductive Reasoning. - Haniel Barbosa; Chantal Keller; Andrew Reynolds 001; Arjun Viswanathan 001; Cesare Tinelli; Clark W. Barrett (LPAR, 2023)

Attack-defense tree-based analysis and optimal defense synthesis for system design. - Baoluo Meng; Arjun Viswanathan 001; Saswata Paul; William Smith; Abha Moitra; Kit Siu; Michael Durling (Innov. Syst. Softw. Eng., 2025)