Franjo Ivancic

Franjo Ivancic

Franjo's research interests include software engineering, automated software testing, static and dynamic program analysis, software verification, model checking, as well as formal modeling and analysis of cyber-physical systems. Before joining Google, he was a Senior Researcher at NEC Laboratories America in Princeton, NJ from 2003-2013. He received his Ph.D. and MSE degrees in Computer and Information Science from the University of Pennsylvania in Philadelphia, PA. Earlier, he received his diploma (Dipl.-Inform.) degree from the Rheinische Friedrich-Wilhelms-University in Bonn, Germany, for his research performed at the Fraunhofer Institute in St. Augustin, Germany. He received the Morris and Dorothy Rubinoff dissertation award from the University of Pennsylvania. More information is available at www.franjo-ivancic.info.
Authored Publications
Google Publications
Other Publications
Sort By
  • Title
  • Title, descending
  • Year
  • Year, descending
    Reducing Time-To-Fix For Fuzzer Bugs
    Rui Abreu
    Hadi Ravanbakhsh
    Ramesh Viswanathan
    36th IEEE/ACM International Conference on Automated Software Engineering(2021)
    Preview abstract At Google, fuzzing C/C++ libraries has discovered tens of thousands of security and robustness bugs. However, these bugs are often reported much after they were introduced. Developers are provided only with fault-inducing test inputs and replication instructions that highlight a crash, but additional debugging information may be needed to localize the cause of the bug. Hence, developers need to spend substantial time debugging the code and identifying commits that introduced the bug. In this paper, we discuss our experience with automating a fuzzing-enabled bisection that pinpoints the commit in which the crash first manifests itself. This ultimately reduces the time critical bugs stay open in our code base. We report on our experience over the past year, which shows that developers fix bugs on average 2.23 times faster when aided by this automated analysis. View details
    SunDew: Systematic Automated Security Testing
    2020 IEEE 13th International Conference on Software Testing, Validation and Verification (ICST), IEEE, {3-3}
    Preview abstract At Google, tens of thousands of security and robustness bugs have been found by fuzzing C and C++ libraries. The various aspects of the SunDew project, one of the projects working on automated scalable techniques related to fuzzing at Google, are presented: how to fuzz, what to fuzz, and how to deal with discovered bugs. First, a distributed fuzzing infrastructure is presented. It allows to cooperatively utilize multiple test generation techniques. Then, a system for automated fuzz driver generation, named FUDGE, is described, which automatically generates fuzz driver candidates for libraries based on existing client code. Running large-scale fuzzing services also causes lots of bugs and vulnerabilities to be reported. Various techniques are presented to provide feedback to developers to reduce the time a known security bug remains open. Finally, challenges and opportunities to incorporate security testing into the general software development workflow are highlighted. View details
    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
    Replay without Recording of Production Bugs for Service Oriented Architectures
    Nipun Arora
    Jonathan Bell
    Gail Kaiser
    Baishakhi Ray
    Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, ACM(2018), pp. 452-463
    Preview abstract Short time-to-localize and time-to-fix for production bugs is extremely important for any 24x7 service-oriented application (SOA). Debugging buggy behavior in deployed applications is hard, as it requires careful reproduction of a similar environment and workload. Prior approaches for automatically reproducing production failures do not scale to large SOA systems. Our key insight is that for many failures in SOA systems (e.g., many semantic and performance bugs), a failure can automatically be reproduced solely by relaying network packets to replicas of suspect services, an insight that we validated through a manual study of 16 real bugs across five different systems. This paper presents Parikshan, an application monitoring framework that leverages user-space virtualization and network proxy technologies to provide a sandbox “debug” environment. In this “debug” environment, developers are free to attach debuggers and analysis tools without impacting performance or correctness of the production environment. In comparison to existing monitoring solutions that can slow down production applications, Parikshan allows application monitoring at significantly lower overhead. View details
    ARC++: Effective Typestate and Lifetime Dependency Analysis
    Xusheng Xiao
    Gogul Balakrishnan
    Naoto Maeda
    Aarti Gupta
    Deepak Chhetri
    ISSTA, ACM(2014), pp. 116-126
    Preview
    Generating Consistent Updates for Software-Defined Network Configurations
    Yifei Yuan
    Cristian Lumezanu
    Shuyuan Zhang
    Aarti Gupta
    HotSDN, ACM(2014)
    Preview
    An Adaptable Rule Placement for Software Defined Networks
    Shuyuan Zhang
    Cristian Lumezanu
    Yifei Yuan
    Aarti Gupta
    Sharad Malik
    DSN, IEEE(2014)
    Preview
    Modeling and analytics for cyber-physical systems in the age of big data
    Abhishek B. Sharma
    Alexandru Niculescu-Mizil
    Haifeng Chen
    Guofei Jiang
    SIGMETRICS Performance Evaluation Review, 41(2014), pp. 74-77
    Scalable and scope-bounded software verification in Varvel
    Gogul Balakrishnan
    Aarti Gupta
    Sriram Sankaranarayanan
    Naoto Maeda
    Takashi Imoto
    Rakesh Pothengil
    Mustafa Hussain
    Automated Software Engineering(2014)
    Probabilistic Temporal Logic Falsification of Cyber-Physical Systems
    Houssam Abbas
    Georgios E. Fainekos
    Sriram Sankaranarayanan
    Aarti Gupta
    ACM Trans. Embedded Comput. Syst., 12(2013), pp. 95
    Feedback-directed unit test generation for C/C++ using concolic execution
    Pranav Garg
    Gogul Balakrishnan
    Naoto Maeda
    Aarti Gupta
    ICSE(2013), pp. 132-141
    Donut Domains: Efficient Non-convex Domains for Abstract Interpretation
    Khalil Ghorbal
    Gogul Balakrishnan
    Naoto Maeda
    Aarti Gupta
    VMCAI(2012), pp. 235-250
    Concurrent Test Generation Using Concolic Multi-trace Analysis
    Niloofar Razavi
    Vineet Kahlon
    Aarti Gupta
    APLAS(2012), pp. 239-255
    Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis
    Jing Yang
    Gogul Balakrishnan
    Naoto Maeda
    Aarti Gupta
    Nishant Sinha
    Sriram Sankaranarayanan
    Naveen Sharma
    CC(2012), pp. 144-164
    Efficient Probabilistic Model Checking of Systems with Ranged Probabilities
    Khalil Ghorbal
    Parasara Sridhar Duggirala
    Vineet Kahlon
    Aarti Gupta
    RP(2012), pp. 107-120
    Editorial: Special Section VCPSS'09
    Georgios E. Fainekos
    Eric Goubault
    Sriram Sankaranarayanan
    ACM Trans. Embedded Comput. Syst., 11(2012), pp. 52
    Modeling and Analyzing the Interaction of C and C++ Strings
    Gogul Balakrishnan
    Naoto Maeda
    Sriram Sankaranarayanan
    Aarti Gupta
    Rakesh Pothengil
    FoVeOOS(2011), pp. 67-85
    DC2: A framework for scalable, scope-bounded software verification
    Gogul Balakrishnan
    Aarti Gupta
    Sriram Sankaranarayanan
    Naoto Maeda
    Hiroki Tokuoka
    Takashi Imoto
    Yoshiaki Miyazaki
    ASE(2011), pp. 133-142
    Interprocedural Exception Analysis for C++
    Prakash Prabhu
    Naoto Maeda
    Gogul Balakrishnan
    Aarti Gupta
    ECOOP(2011), pp. 583-608
    Interprocedural Exception Analysis for C++
    Prakash Prabhu
    Naoto Maeda
    Gogul Balakrishnan
    Aarti Gupta
    25th European Conference on Object-Oriented Programming (ECOOP)(2011)
    Preview abstract C++ Exceptions provide a useful way for dealing with abnormal program behavior, but often lead to irregular interprocedural control flow that complicates compiler optimizations and static analysis. In this paper, we present an interprocedural exception analysis and transformation framework for C++ that captures the control-flow induced by exceptions and transforms it into an exception-free program that is amenable for precise static analysis. Control-flow induced by exceptions is captured in a modular interprocedural exception control-flow graph (IECFG). The IECFG is further refined using a novel interprocedural dataflow analysis algorithm based on a compact representation for a set of types called the Signed-TypeSet domain. The results of the interprocedural analysis are used by a lowering transformation to generate an exception-free C++ program. The lowering transformations do not affect the precision and accuracy of any subsequent program analysis. Our framework handles all the features of synchronous C++ exception handling and all exception sub-typing rules from the C++0x standard. We demonstrate two applications of our framework: (a) automatic inference of exception specifications for C++ functions for documentation, and (b) checking the ``no-throw'' and ``no-leak'' exception-safety properties. View details
    Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems
    Truong Nghiem
    Sriram Sankaranarayanan
    Georgios E. Fainekos
    Aarti Gupta
    George J. Pappas
    HSCC(2010), pp. 211-220
    Scalable and precise program analysis at NEC
    Gogul Balakrishnan
    Malay K. Ganai
    Aarti Gupta
    Vineet Kahlon
    Weihong Li
    Naoto Maeda
    Nadia Papakonstantinou
    Sriram Sankaranarayanan
    Nishant Sinha
    Chao Wang
    FMCAD(2010), pp. 273-274
    Program analysis via satisfiability modulo path programs
    William R. Harris
    Sriram Sankaranarayanan
    Aarti Gupta
    POPL(2010), pp. 71-82
    Numerical stability analysis of floating-point computations using software model checking
    Malay K. Ganai
    Sriram Sankaranarayanan
    Aarti Gupta
    MEMOCODE(2010), pp. 49-58
    Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems
    Sicun Gao
    Malay K. Ganai
    Aarti Gupta
    Sriram Sankaranarayanan
    Edmund M. Clarke
    FMCAD(2010), pp. 81-89
    Inputs of Coma: Static Detection of Denial-of-Service Vulnerabilities
    Richard M. Chang
    Guofei Jiang
    Sriram Sankaranarayanan
    Vitaly Shmatikov
    CSF(2009), pp. 186-199
    Robustness of Model-Based Simulations
    Georgios E. Fainekos
    Sriram Sankaranarayanan
    Aarti Gupta
    RTSS(2009), pp. 345-354
    Refining the control structure of loops using static analysis
    Gogul Balakrishnan
    Sriram Sankaranarayanan
    Aarti Gupta
    EMSOFT(2009), pp. 49-58
    Efficient decision procedure for non-linear arithmetic constraints using CORDIC
    Malay K. Ganai
    FMCAD(2009), pp. 61-68
    Model checking sequential software programs via mixed symbolic analysis
    Zijiang Yang
    Chao Wang
    Aarti Gupta
    ACM Trans. Design Autom. Electr. Syst., 14(2009)
    Foreword: Special issue on numerical software verification
    Sriram Sankaranarayanan
    Chao Wang
    Formal Methods in System Design, 35(2009), pp. 227-228
    Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models
    Aditya Kanade
    Rajeev Alur
    S. Ramesh
    Sriram Sankaranarayanan
    K. C. Shashidhar
    CAV(2009), pp. 430-445
    A hybrid nano-CMOS architecture for defect and fault tolerance
    Muzaffer O. Simsir
    Srihari Cadambi
    Martin Rötteler
    Niraj K. Jha
    JETC, 5(2009)
    Using hardware transactional memory for data race detection
    Shantanu Gupta
    Florin Sultan
    Srihari Cadambi
    Martin Rötteler
    IPDPS(2009), pp. 1-11
    Mining library specifications using inductive logic programming
    Sriram Sankaranarayanan
    Aarti Gupta
    ICSE(2008), pp. 131-140
    Fault-Tolerant Computing Using a Hybrid Nano-CMOS Architecture
    Muzaffer O. Simsir
    Srihari Cadambi
    Martin Rötteler
    Niraj K. Jha
    VLSI Design(2008), pp. 435-440
    SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement
    Gogul Balakrishnan
    Sriram Sankaranarayanan
    Ou Wei
    Aarti Gupta
    SAS(2008), pp. 238-254
    A Policy Iteration Technique for Time Elapse over Template Polyhedra
    Sriram Sankaranarayanan
    Thao Dang
    HSCC(2008), pp. 654-657
    Symbolic Model Checking of Hybrid Systems Using Template Polyhedra
    Sriram Sankaranarayanan
    Thao Dang
    TACAS(2008), pp. 188-202
    Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking
    Aleksandr Zaks
    Zijiang Yang
    Ilya Shlyakhter
    Srihari Cadambi
    Malay K. Ganai
    Aarti Gupta
    Pranav Ashar
    IEEE Trans. on CAD of Integrated Circuits and Systems, 27(2008), pp. 1513-1517
    Efficient SAT-based bounded model checking for software verification
    Zijiang Yang
    Malay K. Ganai
    Aarti Gupta
    Pranav Ashar
    Theor. Comput. Sci., 404(2008), pp. 256-274
    Dynamic inference of likely data preconditions over predicates by tree learning
    Sriram Sankaranarayanan
    Swarat Chaudhuri
    Aarti Gupta
    ISSTA(2008), pp. 295-306
    RaceTM: detecting data races using transactional memory
    Shantanu Gupta
    Florin Sultan
    Srihari Cadambi
    Martin Rötteler
    SPAA(2008), pp. 104-106
    Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra
    Chao Wang
    Zijiang Yang
    Aarti Gupta
    CAV(2007), pp. 352-365
    State space exploration using feedback constraint generation and Monte-Carlo sampling
    Sriram Sankaranarayanan
    Richard M. Chang
    Guofei Jiang
    ESEC/SIGSOFT FSE(2007), pp. 321-330
    Induction in CEGAR for Detecting Counterexamples
    Chao Wang
    Aarti Gupta
    FMCAD(2007), pp. 77-84
    Disjunctive image computation for software verification
    Chao Wang
    Zijiang Yang
    Aarti Gupta
    ACM Trans. Design Autom. Electr. Syst., 12(2007)
    Program Analysis Using Symbolic Ranges
    Sriram Sankaranarayanan
    Aarti Gupta
    SAS(2007), pp. 366-383
    Mixed symbolic representations for model checking software programs
    Zijiang Yang
    Chao Wang
    Aarti Gupta
    MEMOCODE(2006), pp. 17-26
    Predicate abstraction for reachability analysis of hybrid systems
    Rajeev Alur
    Thao Dang
    ACM Trans. Embedded Comput. Syst., 5(2006), pp. 152-199
    Whodunit? Causal Analysis for Counterexamples
    Chao Wang
    Zijiang Yang
    Aarti Gupta
    ATVA(2006), pp. 82-95
    Disjunctive image computation for embedded software verification
    Chao Wang
    Zijiang Yang
    Aarti Gupta
    DATE(2006), pp. 1205-1210
    Static Analysis in Disjunctive Numerical Domains
    Sriram Sankaranarayanan
    Ilya Shlyakhter
    Aarti Gupta
    SAS(2006), pp. 3-17
    Counterexample-guided predicate abstraction of hybrid systems
    Rajeev Alur
    Thao Dang
    Theor. Comput. Sci., 354(2006), pp. 250-271
    Model Checking C Programs Using F-SOFT
    Ilya Shlyakhter
    Aarti Gupta
    Malay K. Ganai
    ICCD(2005), pp. 297-308
    F-Soft: Software Verification Platform
    Zijiang Yang
    Malay K. Ganai
    Aarti Gupta
    Ilya Shlyakhter
    Pranav Ashar
    CAV(2005), pp. 301-306
    Localization and Register Sharing for Predicate Abstraction
    Himanshu Jain
    Aarti Gupta
    Malay K. Ganai
    TACAS(2005), pp. 397-412
    Reasoning About Threads Communicating via Locks
    Vineet Kahlon
    Aarti Gupta
    CAV(2005), pp. 505-518
    Efficient SAT-based Bounded Model Checking for Software Verification
    Pranav Ashar
    Malay K. Ganai
    Aarti Gupta
    Zijiang Yang
    ISoLA (Preliminary proceedings)(2004), pp. 157-164
    Benchmarks for Hybrid Systems Verification
    Ansgar Fehnker
    HSCC(2004), pp. 326-341
    Hierarchical modeling and analysis of embedded systems
    Rajeev Alur
    Thao Dang
    Joel M. Esposito
    Yerang Hur
    Vijay Kumar
    Insup Lee
    Pradyumna Mishra
    George J. Pappas
    Oleg Sokolsky
    Proceedings of the IEEE, 91(2003), pp. 11-28
    Progress on Reachability Analysis of Hybrid Systems Using Predicate Abstraction
    Rajeev Alur
    Thao Dang
    HSCC(2003), pp. 4-19
    Counter-Example Guided Predicate Abstraction of Hybrid Systems
    Rajeev Alur
    Thao Dang
    TACAS(2003), pp. 208-223
    Generating embedded software from hierarchical hybrid models
    Rajeev Alur
    Jesung Kim
    Insup Lee
    Oleg Sokolsky
    LCTES(2003), pp. 171-182
    Visual Programming for Modeling and Simulation of Biomolecular Regulatory Networks
    Rajeev Alur
    Calin Belta
    Vijay Kumar
    Harvey Rubin
    Jonathan Schug
    Oleg Sokolsky
    Jonathan Webb
    HiPC(2002), pp. 702-712
    A Hybrid Dynamical Systems Approach to Intelligent Low-Level Navigation
    Eric Aaron
    Harold C. Sun
    Dimitris N. Metaxas
    CA(2002), pp. 154-163
    Hybrid System Models of Navigation Strategies for Games and Animations
    Eric Aaron
    Dimitris N. Metaxas
    HSCC(2002), pp. 7-20
    Reachability Analysis of Hybrid Systems via Predicate Abstraction
    Rajeev Alur
    Thao Dang
    HSCC(2002), pp. 35-48
    Hybrid Modeling and Simulation of Biomolecular Networks
    Rajeev Alur
    Calin Belta
    HSCC(2001), pp. 19-32
    A Framework for Reasoning about Animation Systems
    Eric Aaron
    Dimitris N. Metaxas
    IVA(2001), pp. 47-60
    Hierarchical Hybrid Modeling of Embedded Systems
    Rajeev Alur
    Thao Dang
    Joel M. Esposito
    Rafael B. Fierro
    Yerang Hur
    Vijay Kumar
    Insup Lee
    Pradyumna Mishra
    George J. Pappas
    Oleg Sokolsky
    EMSOFT(2001), pp. 14-31
    An automatic rule base generation method for fuzzy pattern recognition with multiphased clustering
    Ashutosh Malaviya
    Liliane Peters
    KES (3)(1998), pp. 66-75