Research Interests
- Broad Interests: Computational Logic, Algebra in Computation, Automated Reasoning, Security.
- Theoretical: Unification Theory, Combination Methods in Automated Reasoning, Term-Rewriting, Algebraic Complexity.
- Applied: Formal Verification of Cryptographic Protocols and Algorithms, Software Verification, Automated Reasoning in Security.
Education
I was a postdoctoral fellow in the Formal Methods Section, CHACS of the U.S. Naval Research Lab. Catherine Meadows was my advisor. Prior to that I did my Ph.D. at the University at Albany-SUNY under Paliath Narendran.
Papers, Publications, and Other Research (ORCID, DBLP)
- Knowledge Problems in Protocol Analysis: Extending the Notion of Subterm Convergent
(With Carter Bunch, Saraid Satterfield, Serdar Erbatur, and Christophe Ringeissen)
Logical Methods in Computer Science
Volume 22, Issue 2: 2026
https://doi.org/10.46298/lmcs-22(2:15)2026 - Graph-Embedded Rewrite Systems: Combination and Undecidability Results
(With Serdar Erbatur, Paliath Narendran, and Christophe Ringeissen)
Frontiers of Combining Systems - 15th International Symposium (FroCoS) 2025
Lecture Notes in Computer Science (LNCS) 15979:209--227 2025. - Knowledge Problems vs Unification and Matching: Dichotomy Results
(With Serdar Erbatur, Paliath Narendran, and Christophe Ringeissen)
10th International Conference on Formal Structures for Computation and Deduction (FSCD) 2025
Leibniz International Proceedings in Informatics (LIPIcs) 337: 2025. - Deciding Knowledge Problems Modulo Classes of Permutative Theories
(With Serdar Erbatur, Paliath Narendran, and Christophe Ringeissen)
Logic-Based Program Synthesis and Transformation - 34th International Symposium, (LOPSTR) 2024.
Lecture Notes in Computer Science (LNCS) 14919:47--63 2024. - Knowledge Problems in Security Protocols: Going Beyond Subterm Convergent Theories
(With Saraid Satterfield, Serdar Erbatur, and Christophe Ringeissen)
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Leibniz International Proceedings in Informatics (LIPIcs) 260: 30:1--30:19 2023. - Teaching an Undergraduate 5G Technology and Security Course, and Its Outcomes
(With Veena Ravishankar)
Poster at the 54th ACM Technical Symposium on Computer Science Education (SIGCSE 2023) - A Targeted Study on the Match between Cybersecurity Higher Education Offerings and Workforce Needs
(With Diane Murphy and Nektaria Tryfona)
Virginia Journal of Science 74 (1-2): 1-17 2023. - CryptoSolve: Towards a Tool for the Symbolic Analysis of Cryptographic Algorithms
(With Chichester, et al.)
Proceedings of the 13th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2022)
Electronic Proceedings of Theoretical Computer Science (EPTCS) 370: 147-161 2022. - Combined Hierarchical Matching: the Regular Case
(With Serdar Erbatur and Christophe Ringeissen)
7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)
Volume 228 of Leibniz International Proceedings in Informatics (LIPIcs), 2022. - Non-disjoint Combined Unification and Closure by Equational Paramodulation
(With Serdar Erbatur and Christophe Ringeissen)
Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021
Volume 12941 of Lecture Notes in Computer Science, Springer 2021. - Algorithmic Problems in the Symbolic Approach to the Verification of Automatically Synthesized Cryptosystems.
(With Hai Lin, Christopher Lynch, Catherine A. Meadows, Paliath Narendran, Veena Ravishankar, and Brandon Rozek)
Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021
Volume 12941 of Lecture Notes in Computer Science, Springer 2021. - Terminating Non-disjoint Combined Unification
(With Serdar Erbatur and Christophe Ringeissen)
Logic-Based Program Synthesis and Transformation. LOPSTR 2020.
Volume 12561 of Lecture Notes in Computer Science, Springer 2021. - Computing knowledge in equational extensions of subterm convergent theories
(With Serdar Erbatur and Christophe Ringeissen)
Mathematical Structures in Computer Science 2020, 30(6), 683-709.
Pre-print: permut-subterm-know.pdf - On Asymmetric Unification for the Theory of XOR with a Homomorphism
(With Christopher Lynch, Catherine Meadows, Paliath Narendran, and Veena Ravishankar)
12th International Symposium on Frontiers of Combining Systems (FroCoS 2019)
Pre-print: ach-asymmetric.pdf
- Rule-Based Unification in Combined Theories and the Finite Variant Property
(With Ajay K. Eeralla, Serdar Erbatur, and Christophe Ringeissen)
13th International Conference on Language and Automata Theory and Applications (LATA 2019)
Implementation: BSM
Volume 11417 of Lecture Notes in Computer Science, Springer 2019.
- Knowledge Problems in Equational Extensions of Subterm Convergent Theories (Extended Abstract)
(With Serdar Erbatur and Christophe Ringeissen)
Presented at the 32nd International workshop on Unification (UNIF – 2018) 2018.
- Non-Disjoint Combination with Forward-Closed Theories
(With Serdar Erbatur and Christophe Ringeissen)
Presented at The 31st International workshop on Unification (UNIF-2017), 2017.
- Notions of Knowledge in Combinations of Theories Sharing Constructors
(With Serdar Erbatur and Christophe Ringeissen)
26th International Conference on Automated Deduction (CADE 26)
Volume 10395 of Lecture Notes in Computer Science, pages 60-76, Springer 2017.
- On Unification Modulo One-Sided Distributivity: Algorithms, Variants and Asymmetry
(With Catherine Meadows and Paliath Narendran)
Logical Methods in Computer Science (LMCS) 11(2) 2015.
- Unification and Matching in Hierarchical Combinations of Syntactic Theories
(With Serdar Erbatur, Deepak Kapur, Paliath Narendran and Christophe Ringeissen)
10th International Symposium on Frontiers of Combining Systems (FroCoS'15)
Volume 9322 of Lecture Notes in Computer Science, pages 291-306, Springer 2015.
- Unification modulo a Theory of Pairing Encryption
(With Serdar Erbatur, Kimberly A. Gero, Catherine Meadows, and Paliath Narendran)
Presented at the 29th International workshop on Unification (UNIF – 2015) 2015.
- On Asymmetric Unification and the Combination Problem in Disjoint Theories
(With Serdar Erbatur, Deepak Kapur, Catherine Meadows, Paliath Narendran and Christophe Ringeissen)
17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2014)
Volume 8412 of Lecture Notes in Computer Science, pages 274-288. Springer, 2014.
- On Asymmetric Unification and the Combination Problem in Disjoint Theories (Extended Abstract)
(With Serdar Erbatur and Christophe Ringeissen)
Presented at the 28th International workshop on Unification (UNIF – 2014) 2014.
RISC-Linz Report Series No. 14-06.
- Hierarchical Combination of Matching Algorithms (Extended Abstract)
(With Serdar Erbatur and Christophe Ringeissen)
Presented at the 28th International workshop on Unification (UNIF – 2014) 2014.
RISC-Linz Report Series No. 14-06.
- Hierarchical Combination of Unification Algorithms (Extended Abstract)
(With Serdar Erbatur, Deepak Kapur, Paliath Narendran and Christophe Ringeissen)
Presented at the 27th International workshop on Unification (UNIF - 2013), 2013.
EasyChair Proceedings in Computing (EPiC), 19, 30-34, 2013.
- Hierarchical Combination
(With Serdar Erbatur, Deepak Kapur, Paliath Narendran and Christophe Ringeissen)
24th International Conference on Automated Deduction (CADE-24).
Volume 7898 of Lecture Notes in Computer Science, pages 249-266. Springer, 2013.
- Unification Modulo One-sided Distributivity and its Variants
(With Paliath Narendran)
6th International Joint Conference on Automated Reasoning (IJCAR 2012).
Volume 7364 of Lecture Notes in Computer Science, pages 408-422. Springer, 2012.
- Unification over distributive exponentiation (sub)Theories
(With Serdar Erbatur, Deepak Kapur and Paliath Narendran)
Journal of Automata, Language and Combinatorics (JALC) 16, 109-140, 2011.
- Unification modulo a partial theory of exponentiation
(With Deepak Kapur and Paliath Narendran)
Presented at the 24th International workshop on Unification (UNIF - 2010), 2010.
Electronic Proceedings of Theoretical Computer Science (EPTCS) 42, 12-23.
- On the Complexity of the Tiden-Arnborg Algorithm for Unification modulo One-Sided Distributivity
(With Paliath Narendran and Bibhu Mahapatra)
Presented at the 24th International workshop on Unification (UNIF - 2010) , 2010.
Electronic Proceedings of Theoretical Computer Science (EPTCS) 42, 54-63.
Other
- Special Issue: Annals of Mathematics and Artificial Intelligence
(Special Issue Editor with Temur Kutsia)
Annals of Mathematics and Artificial Intelligence (2022) 90:453–454 - Unification modulo the theory of map
(With Paliath Narendran and Bingqiao Zhou)
Tech Report