I am a Computer Science PhD candidate at the University of Toronto.
My advisor is Marsha Chechik.
My expertise covers a range of areas in formal methods, programming languages, and software engineering. I am mainly interested in ensuring correctness, reliability, and security of software systems. Specifically, my research contributes automated formal techniques and tools for proving software correctness, discovering bugs, and synthesizing correct software. Moreover, my research addresses problems in automated theorem proving and SMT solving that are motivated by verification and program analysis.
Repository of our award-winning, LLVM-based framework for
experimenting with interpolation-based verification,
abstraction-based verification, as well as interesting combinations of both!
(See our TACAS 2012
and SAS 2012 papers for
descriptions of the algorithms in UFO, and our
CAV 2012 paper for a
description of the implementation.)