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.
View project →
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.
View project →
This project area includes our work on automated translation of software across programming languages. Also see related page on KISP lab’s website.
View project →
This project area includes our work on decidability, complexity, automata, regular theories, synthesis, and foundational questions in logic and verification.
View project →