- Nadeem Abdul Hamid, Associate Professor
- Emily Bishop, Undergraduate Research Associate
- Savannah Laudicina, Undergraduate Research Associate
- Dawson Sherwood, Undergraduate Research Assistant
- 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
- Formal verification of KNN-search-based classification algorithm
- Automated reasoning for the permutation relation on lists
-
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