Kevin's research is on creating a framework for reasoning about concurrent programs, with the ultimate goal of verifying multicore seL4.
More contact information is available at the Contact page.