Curriculum Vitae Domagoj Babi
'c
INFORMATION
Email: *****@****.********.***
WWW: http://www.domagoj.info/
Address: Soda Hall 421, Computer Science Division,
University of California,
Berkeley, CA 94720-1776
2008
Ph.D. in Computer Science, University of British Columbia, Canada
EDUCATION
2003
M.Sc. in Computer Science, University of Zagreb, Croatia
2001
Dipl.Ing. in Electrical Engineering, major in industrial electronics, University
of Zagreb,
Croatia
CITIZENSHIP Citizen of Croatia and Canada, US
Permanent ResidentLANGUAGES English, Croatian, passive German
2010 2012 PDF Research Award from the Canadian Natural Science and Engineer-
SELECTED
ing Research Council NSERCfl
HONOURS AND
2005 2007 Microsoft Research Graduate Fellowship
AWARDS
st
2007 1 place, International Satisfiability Modulo Theories competition,
quantifier-free bit-vector arithmetic category
2004 2005 Fulbright Fellowship, declined in order to attend UBC
2004 2005 UBC University Graduate Fellowship
2000 University of Zagreb Rector Award
2012 Princeton University, Computer Science Department
SELECTED INVITED
2012 University of Maryland, College Park, MD, USA
TALKS
2012, 2009 NASA Ames, Moffett Field, USA
2011, 2010 Lawrence Livermore National Lab, Livermore, USA
2011, 2008 Microsoft Research Redmond, Redmond, USA
2011, 2007 Stanford Research Institute, Menlo Park, USA
2011, 2007 Intel, Strategic CAD Labs, Portland, USA
2009, 2007, 2005 Microsoft Research Cambridge, Cambridge, UK
2007 Stanford, Computer Science Department
2007 UC Berkeley, EECS
2007 Carnegie Mellon University, Department of Computer Science
2007 MIT, Computer Science and Artificial Intelligence Laboratory
2007 Schloss Dagstuhl, Wadern, Germany
2007 Max Planck Institute for Software Systems
2010 Program committee member, International Conference on Computer Aided
PROGRAM
Verification CAV 10fl
2010 Program committee member, International Symposium on Stabilization,
COMMITTEE
Safety, and Security of Distributed Systems SSS 10fl
SERVICE
2009 Program committee member, Satisfiability Modulo Theories workshop
SMT 09fl
2008
Co-chair and co-organizer of the Bit-Precise Reasoning workshop affiliated
with CAV 2008fl
1
RESEARCH University of California at Berkeley, Computer Science Division, Berkeley, USA
EXPERIENCE Research Scientist
since Feb 2010
Synopsys,
Mountain View, USA
Senior R&D Eng
. Jul 2009Feb 2010
Fujitsu Labs America, Sunnyvale, USA
Research Consultant
Feb 2009Jun 2009
Cadence Research Laboratories, Berkeley, USA
Research Scientist
Jun 2008Jan 2009
University of British Columbia, Vancouver, Canada
Research Assistant
Sep 2003Aug 2008
Microsoft Research, Redmond, USA
Visiting Graduate Researcher
Apr 2005Jul 2005
University of Zagreb, Zagreb, Croatia
Research and Teaching Assistant
Sep 2001Aug 2003
2010 Advanced Topics in Computer Security UCB CS294-50fl, guest lecturer
TEACHING
2004 Models of Computation UBC CPSC 121fl, teaching assistant
2001 2003 Computer Architecture, Modeling and Simulation at the University of
Zagrebfl, teaching assistant
PROFESSIONAL Panels. NSF panelist in 2011, USA.
SERVICE
Reviewing. Reviewer for International Journal on Software Tools for Technology
Transfer STTTfl, International Conference on Computer Aided Verification CAVfl,
Symposium on Principles of Programming Languages POPLfl, International Static
Analysis Symposium SASfl, Design Automation Conference DACfl, International Con-
ference on Tools and Algorithms for the Construction and Analysis of Systems TACASfl,
Design and Test Europe DATEfl, International Symposium on Automated Technol-
ogy for Verification and Analysis ATVAfl, International Workshop on Satisfiability
Modulo Theories SMTfl, Haifa Verification Conference HVCfl, Asia and South Pacific
Design Automation Conference ASP-DACfl, International Conference on Computer-
Aided Design ICCADfl, IEEE Transactions on Software Engineering.
Involvement in Creation of Standards. Participated in formulation of the Satisfiabil-
ity Modulo Theories SMTfl standard for bit-vector arithmetic QF BVfl, which is now
used as a standard SMT input format.
Creation of Benchmarks. Generated and delivered software verification benchmarks
used in several SMT competitions, generated and made available malware system call
dependency graphs for the benefit of other researchers.
2
2011 Tree automata inference engine Automated library for inference of tree au-
ACADEMIC
tomata from system call dependency graphs. Useful for classifying software
RESEARCH
and recognizing malicious behaviors.
SOFTWARE
2010 Static analysis engine for binary analysis The static analysis engine pre-
sented in the ISSTA 2011 paper.
2008 Calysto extended static checker Scalable extended static checker capable of
handling up to 300 KLOC of code.
2007 Spear bit-vector arithmetic decision procedure Award-winning bit-vector
arithmetic decision procedure, won on the 2007 SMT competition in the bit-
vector arithmetic category.
2005 HyperSAT boolean satisfiability solver Experimental boolean satisfiability
solver, won 3rd place on the 2005 SAT competition in the handcrafted cate-
gory.
BOOKS
1. Domagoj Babi'c and Zvonimir Rakamari'c. Guidebook for Graduate Studies
Abroad, P.O.I.N.T., ISBN: 978-953-99805-1-9, Croatia, 2007. in Croatianfl
THESES
1. Domagoj Babi'c. Exploiting Structure for Scalable Software Verification, Ph.D.
thesis, University of British Columbia, Computer Science Department, Vancou-
ver, Canada, 2008.
2. Domagoj Babi'c. Discrete Cosine Transform Algorithms for FPGA Devices,
M.Sc. thesis, Faculty of El. Eng. and Computing, University of Zagreb, Croatia,
2003.
3. Domagoj Babi'c. Designing RISC processors in FPGA, Dipl.Ing. thesis, Faculty
of El. Eng. and Computing, University of Zagreb, Croatia, 2001. in Croatianfl
PEER-REVIEWED
1. Domagoj Babi'c, Daniel Reynaud, and Dawn Song. Recognizing Malicious
JOURNAL
Software Behaviors with Tree Automata Inference . Formal Methods in System
PUBLICATIONS
TECHNICAL
1. Domagoj Babi'c and Zvonimir Rakamari'c. Asynchronously Communicating
REPORTS
Visibly Pushdown Systems, UCB Technical Report UCB/EECS-2011-108, EECS
Department, University of California, Berkeley, 2011.
2. Domagoj Babi'c and Madanlal Musuvathi. Modular Arithmetic Decision Pro-
cedure, MSR Technical Report TR-2005-114, Microsoft Research, 2005.
PUBLICATIONS IN
1. Domagoj Babi'c and Zvonimir Rakamari'c. Asynchronously Communicating
SUBMISSION OR
Visibly Pushdown Systems .
PREPARATION