Zulip Chat Archive

Stream: job postings

Topic: Postdoc position at University of North Carolina Charlotte


Meera Sridhar (Dec 10 2025 at 00:14):

Project Description:

We are seeking a highly-motivated Postdoctoral Fellow to join our team for the DARPA Bus-based Local Attack Detection and Elimination (BLADE) program, a groundbreaking collaborative project between UNC Charlotte, Electric Power Research Institute (EPRI) and NVIDIA, to secure critical hardware bus systems. This position will lead the formal methods and verification thrust, focusing on providing mathematical assurances for the security of bus-based communications.
Key Responsibilities:

  • Formally model and verify the correctness of “Forensic Observation Data” (FODs) to ensure they accurately detect specified vulnerabilities.

  • Investigate and define formal models of formal security properties of the PCIe bus and NVIDIA’s DPU, CPU, and NIC for the purposes of security.

  • Explore the use of high-assurance languages and toolchains for the implementation of a verified validation engine.

  • Collaborate closely with our systems and cybersecurity teams to integrate formal analysis and verified components into the broader project.

  • Publish research in top-tier security and formal methods conferences and journals.

Required Qualifications:

  • A Ph.D. (or anticipated completion) in Computer Science or a related field.

  • A strong research background in formal methods, with demonstrated experience in model checking, theorem proving, or formal specification.

  • An interest in applying formal methods to real-world systems and security challenges.

Preferred Qualifications:

  • Direct experience with formal specification and verification tools (e.g., Lean, TLA+, Coq, SMT solvers, etc.) is strongly preferred.

  • Familiarity with high-assurance languages or provably-correct software development.

  • Knowledge of low-level hardware protocols (e.g., PCIe), computer architecture, or systems security.

  • Understanding of vulnerability analysis or anomaly detection.

To apply, please submit the following materials to Dr. Meera Sridhar (msridhar@charlotte.edu):

  1. A Curriculum Vitae (CV).

  2. A cover letter detailing your specific experience with formal methods tools and your interest in systems security.

  3. Contact information for three professional references.

  4. One or two representative publications (preferably on formal verification or security).


Last updated: Dec 20 2025 at 21:32 UTC