My research is organized around the following broad areas.
This project area includes our work on concurrency testing and verification. This includes our work on runtime predictive analysis such as prediction of data races, deadlocks, atomicity violations and other classes of properties, as well as linearizability monitoring, model checking, and related verification questions for concurrent systems.
This project area includes my work on hardware description languages, timing-safe hardware, secure hardware design, and related verification and synthesis questions. See Anvil playground.
This project area includes our work on automated translation of software across programming languages. Also see related page on KISP lab’s website.
This project area includes our work on decidability, complexity, automata, regular theories, synthesis, and foundational questions in logic and verification.