My research interests lie mainly in software verification. I am particularly interested in software verification techniques that utilize Craig interpolation as a means for constructing proofs of correctness. More recently, I have started developing techniques for recursive program synthesis.
March 4 2013 I will be at Microsoft Research Cambridge for the next three months.
Dec 16 2012: Our verifier UFO won 4 gold medals and
1 bronze medal at the
International Competition on Software Verification (SV-COMP).
(1) Linux Device Drivers 64-bit,
(2) Control Flow and Integer variables
(Windows device drivers, SSH models, etc.),
(3) SystemC, (4) Product Lines.
Bronze categories: Loops
July 10 2012: The UFO software verification tool and framework is now available!
UFO: A tool and a framework for experimenting with interpolation-based verification,
abstraction-based verification, as well as interesting combinations of both!
(See our TACAS 2012 paper for details.)
Whale: An interpolation-based interprocedural software model checker.
Whale computes function summaries using
interpolants from under-approximations of functions.
(See our VMCAI 2012 paper for details.)