I am a Senior Software Engineer at Google. My interests span program analysis, operating systems, programming languages, and compilers. Here is my CV.
Prior to joining Google, I focused on developing techniques and tools for scaling whitebox automated test generation to real-world systems. To reduce path explosion, large systems are usually broken down into smaller components analyzed in isolation, using simplified representations of the component’s dependencies, i.e., its environment. The core results of my work provide environment representations for accurately and efficiently analyzing systems that are commonly encountered in the real world. To this end, I developed techniques for effective symbolic execution of systems interacting with the operating system (Cloud9) and of programs written in high-level dynamic languages (Chef).
FUDGE: Fuzz Driver Generation at Scale
In ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), Tallinn, Estonia, August 2019
(Best Paper Award)
Prototyping Symbolic Execution Engines for Interpreted Languages
In International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), Salt Lake City, UT, March 2014
Making Automated Testing of Cloud Applications an Integral Component of PaaS
In Asia-Pacific Workshop on Systems (APSYS), Singapore, July 2013
Efficient State Merging in Symbolic Execution
In Conference on Programming Language Design and Implementation (PLDI), Beijing, China, June 2012
Parallel Symbolic Execution for Automated Real-World Software Testing
In ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys), Salzburg, Austria, April 2011
Automated Software Testing as a Service
In ACM Symposium on Cloud Computing (SOCC), Indianapolis, IN, June 2010
Cloud9: A Software Testing Service
In ACM Operating Systems Review (OSR), Vol. 43, No. 4, December 2009
Cloud9 is a symbolic execution platform for low-level system software, such as UNIX utilities, web servers, and distributed systems. Such systems rely on operating system calls to perform their job. To scalably support them in symbolic execution, Cloud9 introduces the idea of a symbolic operating system model that is split between a core set of primitives built into the engine and a full operating system interface emulated inside the symbolic runtime. Our approach requires as few as two primitives to support the POSIX interface: threads with synchronization and address spaces with shared memory.
Cloud9 parallelizes symbolic execution on large clusters of commodity hardware and was the first to demonstrate linear scalability on hundreds of nodes. Cloud9 is available at http://cloud9.epfl.ch.
To manage the complexity of symbolically executing the entire interpreter, Chef employs Class-Uniform Path Analysis (CUPA), an algorithm for prioritizing paths by grouping them into equivalence classes according to a coverage goal. Our Chef prototype generates up to 1000 times more tests in popular Python and Lua packages compared to a plain symbolic execution of the interpreters. Chef is available at http://dslab.epfl.ch/proj/chef/.
A more extensive summary of my work can be found in a (slightly outdated) research statement.