I am a fourth-year PhD candidate in Computer Science at Stony Brook University, advised by Dr. Omar Chowdhury. My research bridges formal methods and large language models to build trustworthy AI systems for security-critical applications — evaluating how reliably LLMs translate natural language into Linear Temporal Logic (LTL), and building a verifier-controlled system that checks natural-language HIPAA compliance questions against a machine-checked Datalog formalization of the law.
Prior to Stony Brook, I completed my M.Sc. at the University of New Brunswick under Dr. Ali Ghorbani, where my work on IoT device profiling has been cited over 220 times.
I am actively seeking Research Scientist Internship positions for Summer 2027 in: AI Safety • Formal Verification • Privacy Compliance • Trustworthy AI
📧 priscillakyeidanso@gmail.com • 💻 GitHub • 📚 Google Scholar
ATHENA studies how large language models can assist with regulatory compliance without giving the language model control over the compliance decision.
Given a question such as “Is this disclosure of protected health information permitted under HIPAA?”, ATHENA uses a machine-checked Datalog encoding of the HIPAA Privacy Rule, executed in Soufflé. Rather than asking an LLM to extract every potentially relevant fact upfront, the verifier determines which unresolved fact can still affect the current policy proof and asks an LLM evidence oracle about that fact. The oracle returns TRUE, FALSE, or UNKNOWN.
A key design principle is that missing evidence remains missing. An UNKNOWN response is preserved as UNRESOLVED rather than silently treated as FALSE. This separates evidence acquisition from policy decision-making: the LLM supplies evidence, while the formal verifier determines which evidence is relevant and whether the policy establishes a permitted or denied outcome.
ATHENA is currently scoped to HIPAA and is being evaluated across real-world disclosure scenarios and multiple language models. A future direction I am exploring is multi-regulatory compliance, where a single data-use scenario may fall under overlapping frameworks—for example, a U.S. healthcare setting in which HIPAA and GDPR obligations may both become relevant. This direction is exploratory and has not yet been implemented.
Under review at PoPETs 2027.
Beyond syntactic correctness, I built a multi-dimensional evaluation framework that scores LLM-generated temporal logic on semantic equivalence and trace-based behavior — the results (LLMs hit only 60–70% semantic accuracy on complex temporal properties) are part of what motivates keeping a symbolic verifier in the loop, as ATHENA does above. This work is published as “Syntax Is Easy, Semantics Is Hard” at ACM SecDev ‘26.
[Under Review, PoPETs 2027] P.K. Danso, et al. “ATHENA: Answering Regulatory Permissibility Questions through Iterative Fact Finding”
[SecDev ‘26] P.K. Danso, et al. “Syntax Is Easy, Semantics Is Hard: Evaluating LLMs for LTL Translation”. Proceedings of the 2026 ACM Secure Development Conference.
[IoT-J 2023] P.K. Danso, S. Dadkhah, E.C.P. Neto, et al. “Transferability of Machine Learning Algorithms for IoT Device Profiling and Identification”. IEEE Internet of Things Journal, 2023.
[PST 2022] S. Dadkhah, H. Mahdikhani, P.K. Danso*, et al. “Towards the Development of a Realistic Multidimensional IoT Profiling Dataset”. IEEE PST, 2022. (220+ citations)
*Equal contribution
Teaching Assistant, Stony Brook University:
Interested in collaborating?
📧 Email: priscillakyeidanso@gmail.com
💼 LinkedIn: linkedin.com/in/priscillakyeidanso
💻 GitHub: github.com/priscilla100
📚 Google Scholar: citations?user=bPvjbUMAAAAJ
Last updated: September 2026