I am a fourth-year PhD candidate in Computer Science at Stony Brook University, advised by Dr. Omar Chowdhury. My research combines LLMs with symbolic analysis and reasoning: LLMs translate natural language into formal logic, and symbolic tools verify, select, and decide. This reduces hallucination and gives formal tools a natural-language interface. I apply it to temporal-logic specification (SecDev ‘26; under review at ICLR 2027) and HIPAA compliance checking (ATHENA; under review at PoPETs 2027).
Previously, I completed my M.Sc. at the University of New Brunswick under Dr. Ali Ghorbani; my IoT device profiling work 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.
PoPETs 2027 (Issue 2): advanced to Round 2 of review.
A natural-language requirement can admit several plausible temporal-logic formalizations, so generating a correct candidate is not the same as selecting the intended one. Pendulum separates candidate synthesis from symbolic semantic analysis and final selection: solver-backed (BLACK) equivalence and behavioral evidence is assessed by an LLM judge, and deterministic finalization commits to one formula.
On the nl2ltl benchmark, after auditing all 306 references (55 corrected, 48 ambiguous specifications kept as a separate partition), the strongest candidate pool contains a correct formula for 92.2% of the 258 determinate specifications, but the final system selects one correctly for 87.2%. This coverage-to-selection gap persists across changes to synthesis, verification, and selection.
Under review at ICLR 2027 · OpenReview
A multi-dimensional evaluation framework that scores LLM-generated temporal logic on syntactic well-formedness, semantic equivalence, and trace-based behavior. Best-observed equivalence accuracy on NL→LTL translation stays around 65–73% across prompting interfaces, which motivates keeping symbolic tools in the loop, as in the two projects above. Published at ACM SecDev ‘26.
[Under Review, ICLR 2027] P.K. Danso, et al. “Generation Is Not Selection: Neuro-Symbolic Natural Language Formalization of Temporal Logic”. OpenReview
[Under Review, PoPETs 2027 · Round 2] 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