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).

Previous Publications

  •  

    Asynchronously Communicating Visibly Pushdown Systems

    Domagoj Babic, Zvonimir Rakamaric

    Proceedings of the 2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems, Springer, pp. 225-242

  •  

    Proving termination of nonlinear command sequences

    Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric

    Formal Asp. Comput., vol. 25 (2013), pp. 389-403

  •  

    Sigma*: symbolic learning of input-output specifications

    Matko Botincan, Domagoj Babic

    POPL (2013), pp. 443-456

  •  

    Recognizing malicious software behaviors with tree automata inference

    Domagoj Babic, Daniel Reynaud, Dawn Song

    Formal Methods in System Design, vol. 41 (2012), pp. 107-128

  •  

    MACE: Model-inference-Assisted Concolic Exploration for Protocol and Vulnerability Discovery

    Chia Yuan Cho, Domagoj Babic, Pongsin Poosankam, Kevin Zhijie Chen, Edward XueJun Wu, Dawn Song

    USENIX Security Symposium (2011)

  •  

    Malware Analysis with Tree Automata Inference

    Domagoj Babic, Daniel Reynaud, Dawn Song

    CAV (2011), pp. 116-131

  •  

    Statically-directed dynamic automated test generation

    Domagoj Babic, Lorenzo Martignoni, Stephen McCamant, Dawn Song

    ISSTA (2011), pp. 12-22

  •  

    Inference and analysis of formal models of botnet command and control protocols

    Chia Yuan Cho, Domagoj Babic, Eui Chul Richard Shin, Dawn Song

    ACM Conference on Computer and Communications Security (2010), pp. 426-439

  •  

    Input generation via decomposition and re-stitching: finding bugs in Malware

    Juan Caballero, Pongsin Poosankam, Stephen McCamant, Domagoj Babic, Dawn Song

    ACM Conference on Computer and Communications Security (2010), pp. 413-425

  •  

    Approximating the safely reusable set of learned facts

    Domagoj Babic, Alan J. Hu

    STTT, vol. 11 (2009), pp. 325-338

  •  

    Calysto: scalable and precise extended static checking

    Domagoj Babic, Alan J. Hu

    ICSE (2008), pp. 211-220

  •  

    Boosting Verification by Automatic Tuning of Decision Procedures

    Frank Hutter, Domagoj Babic, Holger H. Hoos, Alan J. Hu

    FMCAD (2007), pp. 27-34

  •  

    Exploiting Shared Structure in Software Verification Conditions

    Domagoj Babic, Alan J. Hu

    Haifa Verification Conference (2007), pp. 169-184

  •  

    Proving Termination by Divergence

    Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, Byron Cook

    SEFM (2007), pp. 93-102

  •  

    Structural Abstraction of Software Verification Conditions

    Domagoj Babic, Alan J. Hu

    CAV (2007), pp. 366-378

  •  

    B-Cubing: New Possibilities for Efficient SAT-Solving

    Domagoj Babic, Jesse D. Bingham, Alan J. Hu

    IEEE Trans. Computers, vol. 55 (2006), pp. 1315-1324

  •  

    B-cubing theory: new possibilities for efficient SAT-solving

    Domagoj Babic, Jesse D. Bingham, Alan J. Hu

    HLDVT (2005), pp. 192-199

  •  

    Efficient SAT solving: beyond supercubes

    Domagoj Babic, Jesse D. Bingham, Alan J. Hu

    DAC (2005), pp. 744-749

  •  

    Integration of supercubing and learning in a SAT solver

    Domagoj Babic, Alan J. Hu

    ASP-DAC (2005), pp. 438-444