Jump to Content
Domagoj Babic

Domagoj Babic

I joined Google in April 2013 and I'm currently a Staff Research Scientist, tech lead, and manager. My work focuses on research and development of automated software analysis systems for various security-related applications. Primarily, I want my work to have a positive impact on people's lives. I enjoy building top-notch teams and working with them on solving large-scale real-world important problems, while learning and having fun on the way. I'm particularly excited about big technical challenges and enjoy creating the vision, strategy, and technology for taming those challenges.

Over my career, I've published in the areas of verification, testing, security of complex software systems, automated reasoning, grammar inference, and applied formal methods. Before joining Google, I was a research scientist at UC Berkeley and elsewhere in industry.

I earned my Dipl.Ing. in Electrical Engineering and M.Sc. in Computer Science from the Zagreb University (Faculty of Electrical Engineering and Computing) in 2001 and 2003. I received a Ph.D. in Computer Science in 2008 from the University of British Columbia. I was a recipient of the NSERC PDF Research Fellowship (2010-2012), Microsoft Graduate Research Fellowship (2005-2007), and several awards at international programming competitions (1st place at the 2007 Satisfiability Modulo Theories competition in the bit-vector arithmetic category and 3rd place at the 2005 Satisfiability Testing competition in the satisfiable-crafted instances category).
Authored Publications
Google Publications
Other Publications
Sort By
  • Title
  • Title, descending
  • Year
  • Year, descending
    FUDGE: Fuzz Driver Generation at Scale
    Yaohui Chen
    Markus Kusano
    Caroline Lemieux
    Wei Wang
    Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ACM
    Preview abstract At Google we have found tens of thousands of security and robustness bugs by fuzzing C and C++ libraries. To fuzz a library, a fuzzer requires a fuzz driver—which exercises some library code—to which it can pass inputs. Unfortunately, writing fuzz drivers remains a primarily manual exercise, a major hindrance to the widespread adoption of fuzzing. In this paper, we address this major hindrance by introducing the Fudge system for automated fuzz driver generation. Fudge automatically generates fuzz driver candidates for libraries based on existing client code. We have used Fudge to generate thousands of new drivers for a wide variety of libraries. Each generated driver includes a synthesized C/C++ program and a corresponding build script, and is automatically analyzed for quality. Developers have integrated over 200 of these generated drivers into continuous fuzzing services and have committed to address reported security bugs. Further, several of these fuzz drivers have been upstreamed to open source projects and integrated into the OSS-Fuzz fuzzing infrastructure. Running these fuzz drivers has resulted in over 150 bug fixes, including the elimination of numerous exploitable security vulnerabilities. View details
    Proving termination of nonlinear command sequences
    Byron Cook
    Alan J. Hu
    Zvonimir Rakamaric
    Formal Asp. Comput., vol. 25 (2013), pp. 389-403
    Asynchronously Communicating Visibly Pushdown Systems
    Zvonimir Rakamaric
    Proceedings of the 2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems, Springer, pp. 225-242
    Sigma*: symbolic learning of input-output specifications
    Matko Botincan
    POPL (2013), pp. 443-456
    Recognizing malicious software behaviors with tree automata inference
    Daniel Reynaud
    Dawn Song
    Formal Methods in System Design, vol. 41 (2012), pp. 107-128
    Statically-directed dynamic automated test generation
    Lorenzo Martignoni
    Stephen McCamant
    Dawn Song
    ISSTA (2011), pp. 12-22
    MACE: Model-inference-Assisted Concolic Exploration for Protocol and Vulnerability Discovery
    Chia Yuan Cho
    Pongsin Poosankam
    Kevin Zhijie Chen
    Edward XueJun Wu
    Dawn Song
    USENIX Security Symposium (2011)
    Malware Analysis with Tree Automata Inference
    Daniel Reynaud
    Dawn Song
    CAV (2011), pp. 116-131
    Input generation via decomposition and re-stitching: finding bugs in Malware
    Juan Caballero
    Pongsin Poosankam
    Stephen McCamant
    Dawn Song
    ACM Conference on Computer and Communications Security (2010), pp. 413-425
    Inference and analysis of formal models of botnet command and control protocols
    Chia Yuan Cho
    Eui Chul Richard Shin
    Dawn Song
    ACM Conference on Computer and Communications Security (2010), pp. 426-439
    Approximating the safely reusable set of learned facts
    Alan J. Hu
    STTT, vol. 11 (2009), pp. 325-338
    Calysto: scalable and precise extended static checking
    Alan J. Hu
    ICSE (2008), pp. 211-220
    Proving Termination by Divergence
    Alan J. Hu
    Zvonimir Rakamaric
    Byron Cook
    SEFM (2007), pp. 93-102
    Boosting Verification by Automatic Tuning of Decision Procedures
    Frank Hutter
    Holger H. Hoos
    Alan J. Hu
    FMCAD (2007), pp. 27-34
    Exploiting Shared Structure in Software Verification Conditions
    Alan J. Hu
    Haifa Verification Conference (2007), pp. 169-184
    Structural Abstraction of Software Verification Conditions
    Alan J. Hu
    CAV (2007), pp. 366-378
    B-Cubing: New Possibilities for Efficient SAT-Solving
    Jesse D. Bingham
    Alan J. Hu
    IEEE Trans. Computers, vol. 55 (2006), pp. 1315-1324
    B-cubing theory: new possibilities for efficient SAT-solving
    Jesse D. Bingham
    Alan J. Hu
    HLDVT (2005), pp. 192-199
    Efficient SAT solving: beyond supercubes
    Jesse D. Bingham
    Alan J. Hu
    DAC (2005), pp. 744-749
    Integration of supercubing and learning in a SAT solver
    Alan J. Hu
    ASP-DAC (2005), pp. 438-444