People

Current

• Nadeem Abdul Hamid, Associate Professor
• Emily Bishop, Undergraduate Research Associate
• Savannah Laudicina, Undergraduate Research Associate
• Dawson Sherwood, Undergraduate Research Assistant

Former/Alumni

• Great Abhieyighan, Undergraduate Research Assistant
• Matthew Bowker, Undergraduate Research Assistant
• Jessica Herring, Undergraduate Research Assistant
• Bernny Velasquez, Lead Undergraduate Research Associate
• Bella Vos, Undergraduate Research Assistant

Projects

• Formal verification of KNN-search-based classification algorithm
• Automated reasoning for the permutation relation on lists

Publications

• Nadeem Abdul Hamid, 2025. Towards Automating Permutation Proofs in Rocq: A Reflexive Approach with Iterative Deepening Search (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 39:1-39:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

  Rocq tactic implementation

• Bernny Velasquez, Jessica Herring, and Nadeem Abdul Hamid. Formally Verified Implementation of the K-Nearest Neighbors Classification Algorithm.. In C. Nogueira, S., Teodorov, C. (eds) Formal Methods: Foundations and Applications. SBMF 2024. Lecture Notes in Computer Science, vol 15403. Springer, Cham.

  Coq developments

  slides

• Nadeem Abdul Hamid. 2024. (Nearest) Neighbors You Can Rely On: Formally Verified k-d Tree Construction and Search in Coq. In Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing (SAC ‘24) [Software Verification and Testing (SVT) track].

  Coq developments arxiv preprint

  slides