Formal Methods · Static Analysis . Programming Languages · Systems Security

My research interests span formal methods, static analysis, programming languages, software security, and the application of formal methods across diverse areas of computer science. I develop machine-checked proofs using the Rocq(formerly Coq) proof assistant to establish strong correctness and security guarantees, with the broader goal of building trustworthy computing systems. Much of my research is carried out using Rocq.

Portrait of Swarn Priya

Overview

About me

I am a Research Assistant Professor in the School of Electrical Engineering and Computer Science at Washington State University.

Before joining WSU, I was a Postdoctoral Research Associate in the Systems Software Research Groupwithin the Bradley Department of Electrical and Computer Engineering at Virginia Tech. During this time, I led the development of BeePL, a formally verified programming language and compiler for eBPF that aims to provide machine-checked guarantees of safety, correctness, and security for systems software. I received my Ph.D. from Inria, Sophia Antipolis and Université Côte d'Azur, France, where I worked with Yves Bertot and Benjamin Grégoire as a member of the STAMP and SPLiTS research teams. My Ph.D. research focused on applying formal methods to computer security, with an emphasis on designing a formally verified secure compiler that provides machine-checked guarantees against timing-based side-channel attacks.

Read more about my research →

Selected work

Publications

All publications →
2025

BeePL: Correct-by-compilation kernel extensions

Swarn Priya, Frédéric Besson, Connor Sughrue, Tim Steenvoorden, Jamie Fulford, Freek Verbeek, and Binoy Ravindran

arXiv

2025

BeePL: Correct-by-compilation kernel extensions

Swarn Priya, Tim Steenvoorden, Connor Sughrue, Frédéric Besson, and Freek Verbeek

Workshop on Principles of Secure Compilation (PriSC)

2023

Formally computer-verified protections against timing-based side-channel attacks

Swarn Priya

Ph.D. thesis, Inria and Université Côte d’Azur

2023

Typing High-Speed Cryptography against Spectre v1

Basavesh A. Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, and Lucas Tabary-Maujean

Alphabetical authorship

IEEE Symposium on Security and Privacy (S&P)