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
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
Preview
Xusheng Xiao
Naoto Maeda
Aarti Gupta
Deepak Chhetri
ISSTA, ACM (2014), pp. 116-126
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, vol. 41 (2014), pp. 74-77
Scalable and scope-bounded software verification in Varvel
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., vol. 12 (2013), pp. 95
Feedback-directed unit test generation for C/C++ using concolic execution
Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis
Jing Yang
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
Concurrent Test Generation Using Concolic Multi-trace Analysis
Donut Domains: Efficient Non-convex Domains for Abstract Interpretation
Editorial: Special Section VCPSS'09
Georgios E. Fainekos
Eric Goubault
Sriram Sankaranarayanan
ACM Trans. Embedded Comput. Syst., vol. 11 (2012), pp. 52
DC2: A framework for scalable, scope-bounded software verification
Aarti Gupta
Sriram Sankaranarayanan
Naoto Maeda
Hiroki Tokuoka
Takashi Imoto
Yoshiaki Miyazaki
ASE (2011), pp. 133-142
Interprocedural Exception Analysis for C++
Naoto Maeda
Gogul Balakrishnan
Aarti Gupta
25th European Conference on Object-Oriented Programming (ECOOP) (2011)
Interprocedural Exception Analysis for C++
Modeling and Analyzing the Interaction of C and C++ Strings
Naoto Maeda
Sriram Sankaranarayanan
Aarti Gupta
Rakesh Pothengil
FoVeOOS (2011), pp. 67-85
Numerical stability analysis of floating-point computations using software model checking
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
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
Program analysis via satisfiability modulo path programs
Scalable and precise program analysis at NEC
Malay K. Ganai
Aarti Gupta
Vineet Kahlon
Weihong Li
Naoto Maeda
Nadia Papakonstantinou
Sriram Sankaranarayanan
Nishant Sinha
Chao Wang
FMCAD (2010), pp. 273-274
Model checking sequential software programs via mixed symbolic analysis
Zijiang Yang
Chao Wang
Aarti Gupta
ACM Trans. Design Autom. Electr. Syst., vol. 14 (2009)
Robustness of Model-Based Simulations
Refining the control structure of loops using static analysis
Foreword: Special issue on numerical software verification
Sriram Sankaranarayanan
Chao Wang
Formal Methods in System Design, vol. 35 (2009), pp. 227-228
Inputs of Coma: Static Detection of Denial-of-Service Vulnerabilities
Richard M. Chang
Guofei Jiang
Sriram Sankaranarayanan
Vitaly Shmatikov
CSF (2009), pp. 186-199
Using hardware transactional memory for data race detection
A hybrid nano-CMOS architecture for defect and fault tolerance
Efficient decision procedure for non-linear arithmetic constraints using CORDIC
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
Symbolic Model Checking of Hybrid Systems Using Template Polyhedra
SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement
Sriram Sankaranarayanan
Ou Wei
Aarti Gupta
SAS (2008), pp. 238-254
Efficient SAT-based bounded model checking for software verification
Zijiang Yang
Malay K. Ganai
Aarti Gupta
Pranav Ashar
Theor. Comput. Sci., vol. 404 (2008), pp. 256-274
Dynamic inference of likely data preconditions over predicates by tree learning
A Policy Iteration Technique for Time Elapse over Template Polyhedra
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, vol. 27 (2008), pp. 1513-1517
RaceTM: detecting data races using transactional memory
Shantanu Gupta
Florin Sultan
Srihari Cadambi
Martin Rötteler
SPAA (2008), pp. 104-106
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
Mining library specifications using inductive logic programming
Program Analysis Using Symbolic Ranges
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
Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra
Disjunctive image computation for software verification
Chao Wang
Zijiang Yang
Aarti Gupta
ACM Trans. Design Autom. Electr. Syst., vol. 12 (2007)
Induction in CEGAR for Detecting Counterexamples
Counterexample-guided predicate abstraction of hybrid systems
Mixed symbolic representations for model checking software programs
Whodunit? Causal Analysis for Counterexamples
Disjunctive image computation for embedded software verification
Predicate abstraction for reachability analysis of hybrid systems
Static Analysis in Disjunctive Numerical Domains
Model Checking C Programs Using F-SOFT
Reasoning About Threads Communicating via Locks
Localization and Register Sharing for Predicate Abstraction
F-Soft: Software Verification Platform
Zijiang Yang
Malay K. Ganai
Aarti Gupta
Ilya Shlyakhter
Pranav Ashar
CAV (2005), pp. 301-306
Benchmarks for Hybrid Systems Verification
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
Progress on Reachability Analysis of Hybrid Systems Using Predicate Abstraction
Generating embedded software from hierarchical hybrid models
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, vol. 91 (2003), pp. 11-28
Counter-Example Guided Predicate Abstraction of Hybrid Systems
Hybrid System Models of Navigation Strategies for Games and Animations
A Hybrid Dynamical Systems Approach to Intelligent Low-Level Navigation
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
Reachability Analysis of Hybrid Systems via Predicate Abstraction
A Framework for Reasoning about Animation Systems
Hybrid Modeling and Simulation of Biomolecular Networks
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
