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.

Google Publications

  •   

    ARC++: Effective Typestate and Lifetime Dependency Analysis

    Xusheng Xiao, Gogul Balakrishnan, Franjo Ivancic, Naoto Maeda, Aarti Gupta, Deepak Chhetri

    ISSTA, ACM (2014), pp. 116-126

  •  

    An Adaptable Rule Placement for Software Defined Networks

    Shuyuan Zhang, Franjo Ivancic, Cristian Lumezanu, Yifei Yuan, Aarti Gupta, Sharad Malik

    DSN, IEEE (2014)

  •   

    Generating Consistent Updates for Software-Defined Network Configurations

    Yifei Yuan, Franjo Ivancic, Cristian Lumezanu, Shuyuan Zhang, Aarti Gupta

    HotSDN, ACM (2014)

Previous Publications

  •  

    Modeling and analytics for cyber-physical systems in the age of big data

    Abhishek B. Sharma, Franjo Ivancic, 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

    Franjo Ivancic, Gogul Balakrishnan, Aarti Gupta, Sriram Sankaranarayanan, Naoto Maeda, Takashi Imoto, Rakesh Pothengil, Mustafa Hussain

    Automated Software Engineering (2014)

  •   

    Feedback-directed unit test generation for C/C++ using concolic execution

    Pranav Garg, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta

    ICSE (2013), pp. 132-141

  •  

    Probabilistic Temporal Logic Falsification of Cyber-Physical Systems

    Houssam Abbas, Georgios E. Fainekos, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta

    ACM Trans. Embedded Comput. Syst., vol. 12 (2013), pp. 95

  •  

    Concurrent Test Generation Using Concolic Multi-trace Analysis

    Niloofar Razavi, Franjo Ivancic, Vineet Kahlon, Aarti Gupta

    APLAS (2012), pp. 239-255

  •  

    Donut Domains: Efficient Non-convex Domains for Abstract Interpretation

    Khalil Ghorbal, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta

    VMCAI (2012), pp. 235-250

  •  

    Editorial: Special Section VCPSS'09

    Georgios E. Fainekos, Eric Goubault, Franjo Ivancic, Sriram Sankaranarayanan

    ACM Trans. Embedded Comput. Syst., vol. 11 (2012), pp. 52

  •  

    Efficient Probabilistic Model Checking of Systems with Ranged Probabilities

    Khalil Ghorbal, Parasara Sridhar Duggirala, Vineet Kahlon, Franjo Ivancic, Aarti Gupta

    RP (2012), pp. 107-120

  •  

    Object Model Construction for Inheritance in C++ and Its Applications to Program Analysis

    Jing Yang, Gogul Balakrishnan, Naoto Maeda, Franjo Ivancic, Aarti Gupta, Nishant Sinha, Sriram Sankaranarayanan, Naveen Sharma

    CC (2012), pp. 144-164

  •  

    DC2: A framework for scalable, scope-bounded software verification

    Franjo Ivancic, 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, Franjo Ivancic, Aarti Gupta

    ECOOP (2011), pp. 583-608

  •  

    Modeling and Analyzing the Interaction of C and C++ Strings

    Gogul Balakrishnan, Naoto Maeda, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta, Rakesh Pothengil

    FoVeOOS (2011), pp. 67-85

  •  

    Integrating ICP and LRA solvers for deciding nonlinear real arithmetic problems

    Sicun Gao, Malay K. Ganai, Franjo Ivancic, 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, Franjo Ivancic, Aarti Gupta, George J. Pappas

    HSCC (2010), pp. 211-220

  •  

    Numerical stability analysis of floating-point computations using software model checking

    Franjo Ivancic, Malay K. Ganai, Sriram Sankaranarayanan, Aarti Gupta

    MEMOCODE (2010), pp. 49-58

  •  

    Program analysis via satisfiability modulo path programs

    William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta

    POPL (2010), pp. 71-82

  •  

    Scalable and precise program analysis at NEC

    Gogul Balakrishnan, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Vineet Kahlon, Weihong Li, Naoto Maeda, Nadia Papakonstantinou, Sriram Sankaranarayanan, Nishant Sinha, Chao Wang

    FMCAD (2010), pp. 273-274

  •  

    A hybrid nano-CMOS architecture for defect and fault tolerance

    Muzaffer O. Simsir, Srihari Cadambi, Franjo Ivancic, Martin Rötteler, Niraj K. Jha

    JETC, vol. 5 (2009)

  •  

    Efficient decision procedure for non-linear arithmetic constraints using CORDIC

    Malay K. Ganai, Franjo Ivancic

    FMCAD (2009), pp. 61-68

  •  

    Foreword: Special issue on numerical software verification

    Franjo Ivancic, Sriram Sankaranarayanan, Chao Wang

    Formal Methods in System Design, vol. 35 (2009), pp. 227-228

  •  

    Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models

    Aditya Kanade, Rajeev Alur, Franjo Ivancic, S. Ramesh, Sriram Sankaranarayanan, K. C. Shashidhar

    CAV (2009), pp. 430-445

  •  

    Inputs of Coma: Static Detection of Denial-of-Service Vulnerabilities

    Richard M. Chang, Guofei Jiang, Franjo Ivancic, Sriram Sankaranarayanan, Vitaly Shmatikov

    CSF (2009), pp. 186-199

  •  

    Model checking sequential software programs via mixed symbolic analysis

    Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivancic

    ACM Trans. Design Autom. Electr. Syst., vol. 14 (2009)

  •  

    Refining the control structure of loops using static analysis

    Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta

    EMSOFT (2009), pp. 49-58

  •  

    Robustness of Model-Based Simulations

    Georgios E. Fainekos, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta

    RTSS (2009), pp. 345-354

  •  

    Using hardware transactional memory for data race detection

    Shantanu Gupta, Florin Sultan, Srihari Cadambi, Franjo Ivancic, Martin Rötteler

    IPDPS (2009), pp. 1-11

  •  

    A Policy Iteration Technique for Time Elapse over Template Polyhedra

    Sriram Sankaranarayanan, Thao Dang, Franjo Ivancic

    HSCC (2008), pp. 654-657

  •  

    Bitwidth Reduction via Symbolic Interval Analysis for Software Model Checking

    Aleksandr Zaks, Zijiang Yang, Ilya Shlyakhter, Franjo Ivancic, Srihari Cadambi, Malay K. Ganai, Aarti Gupta, Pranav Ashar

    IEEE Trans. on CAD of Integrated Circuits and Systems, vol. 27 (2008), pp. 1513-1517

  •  

    Dynamic inference of likely data preconditions over predicates by tree learning

    Sriram Sankaranarayanan, Swarat Chaudhuri, Franjo Ivancic, Aarti Gupta

    ISSTA (2008), pp. 295-306

  •  

    Efficient SAT-based bounded model checking for software verification

    Franjo Ivancic, Zijiang Yang, Malay K. Ganai, Aarti Gupta, Pranav Ashar

    Theor. Comput. Sci., vol. 404 (2008), pp. 256-274

  •  

    Fault-Tolerant Computing Using a Hybrid Nano-CMOS Architecture

    Muzaffer O. Simsir, Srihari Cadambi, Franjo Ivancic, Martin Rötteler, Niraj K. Jha

    VLSI Design (2008), pp. 435-440

  •  

    Mining library specifications using inductive logic programming

    Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta

    ICSE (2008), pp. 131-140

  •  

    RaceTM: detecting data races using transactional memory

    Shantanu Gupta, Florin Sultan, Srihari Cadambi, Franjo Ivancic, Martin Rötteler

    SPAA (2008), pp. 104-106

  •  

    SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement

    Gogul Balakrishnan, Sriram Sankaranarayanan, Franjo Ivancic, Ou Wei, Aarti Gupta

    SAS (2008), pp. 238-254

  •  

    Symbolic Model Checking of Hybrid Systems Using Template Polyhedra

    Sriram Sankaranarayanan, Thao Dang, Franjo Ivancic

    TACAS (2008), pp. 188-202

  •  

    Disjunctive image computation for software verification

    Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta

    ACM Trans. Design Autom. Electr. Syst., vol. 12 (2007)

  •  

    Induction in CEGAR for Detecting Counterexamples

    Chao Wang, Aarti Gupta, Franjo Ivancic

    FMCAD (2007), pp. 77-84

  •  

    Program Analysis Using Symbolic Ranges

    Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta

    SAS (2007), pp. 366-383

  •  

    State space exploration using feedback constraint generation and Monte-Carlo sampling

    Sriram Sankaranarayanan, Richard M. Chang, Guofei Jiang, Franjo Ivancic

    ESEC/SIGSOFT FSE (2007), pp. 321-330

  •  

    Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra

    Chao Wang, Zijiang Yang, Aarti Gupta, Franjo Ivancic

    CAV (2007), pp. 352-365

  •  

    Counterexample-guided predicate abstraction of hybrid systems

    Rajeev Alur, Thao Dang, Franjo Ivancic

    Theor. Comput. Sci., vol. 354 (2006), pp. 250-271

  •  

    Disjunctive image computation for embedded software verification

    Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta

    DATE (2006), pp. 1205-1210

  •  

    Mixed symbolic representations for model checking software programs

    Zijiang Yang, Chao Wang, Aarti Gupta, Franjo Ivancic

    MEMOCODE (2006), pp. 17-26

  •  

    Predicate abstraction for reachability analysis of hybrid systems

    Rajeev Alur, Thao Dang, Franjo Ivancic

    ACM Trans. Embedded Comput. Syst., vol. 5 (2006), pp. 152-199

  •  

    Static Analysis in Disjunctive Numerical Domains

    Sriram Sankaranarayanan, Franjo Ivancic, Ilya Shlyakhter, Aarti Gupta

    SAS (2006), pp. 3-17

  •  

    Whodunit? Causal Analysis for Counterexamples

    Chao Wang, Zijiang Yang, Franjo Ivancic, Aarti Gupta

    ATVA (2006), pp. 82-95

  •  

    F-Soft: Software Verification Platform

    Franjo Ivancic, 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, Franjo Ivancic, Aarti Gupta, Malay K. Ganai

    TACAS (2005), pp. 397-412

  •  

    Model Checking C Programs Using F-SOFT

    Franjo Ivancic, Ilya Shlyakhter, Aarti Gupta, Malay K. Ganai

    ICCD (2005), pp. 297-308

  •  

    Reasoning About Threads Communicating via Locks

    Vineet Kahlon, Franjo Ivancic, Aarti Gupta

    CAV (2005), pp. 505-518

  •  

    Benchmarks for Hybrid Systems Verification

    Ansgar Fehnker, Franjo Ivancic

    HSCC (2004), pp. 326-341

  •  

    Efficient SAT-based Bounded Model Checking for Software Verification

    Pranav Ashar, Malay K. Ganai, Aarti Gupta, Franjo Ivancic, Zijiang Yang

    ISoLA (Preliminary proceedings) (2004), pp. 157-164

  •  

    Counter-Example Guided Predicate Abstraction of Hybrid Systems

    Rajeev Alur, Thao Dang, Franjo Ivancic

    TACAS (2003), pp. 208-223

  •  

    Generating embedded software from hierarchical hybrid models

    Rajeev Alur, Franjo Ivancic, Jesung Kim, Insup Lee, Oleg Sokolsky

    LCTES (2003), pp. 171-182

  •  

    Hierarchical modeling and analysis of embedded systems

    Rajeev Alur, Thao Dang, Joel M. Esposito, Yerang Hur, Franjo Ivancic, Vijay Kumar, Insup Lee, Pradyumna Mishra, George J. Pappas, Oleg Sokolsky

    Proceedings of the IEEE, vol. 91 (2003), pp. 11-28

  •  

    Progress on Reachability Analysis of Hybrid Systems Using Predicate Abstraction

    Rajeev Alur, Thao Dang, Franjo Ivancic

    HSCC (2003), pp. 4-19

  •  

    A Hybrid Dynamical Systems Approach to Intelligent Low-Level Navigation

    Eric Aaron, Harold C. Sun, Franjo Ivancic, Dimitris N. Metaxas

    CA (2002), pp. 154-163

  •  

    Hybrid System Models of Navigation Strategies for Games and Animations

    Eric Aaron, Franjo Ivancic, Dimitris N. Metaxas

    HSCC (2002), pp. 7-20

  •  

    Reachability Analysis of Hybrid Systems via Predicate Abstraction

    Rajeev Alur, Thao Dang, Franjo Ivancic

    HSCC (2002), pp. 35-48

  •  

    Visual Programming for Modeling and Simulation of Biomolecular Regulatory Networks

    Rajeev Alur, Calin Belta, Franjo Ivancic, Vijay Kumar, Harvey Rubin, Jonathan Schug, Oleg Sokolsky, Jonathan Webb

    HiPC (2002), pp. 702-712

  •  

    A Framework for Reasoning about Animation Systems

    Eric Aaron, Dimitris N. Metaxas, Franjo Ivancic

    IVA (2001), pp. 47-60

  •  

    Hierarchical Hybrid Modeling of Embedded Systems

    Rajeev Alur, Thao Dang, Joel M. Esposito, Rafael B. Fierro, Yerang Hur, Franjo Ivancic, Vijay Kumar, Insup Lee, Pradyumna Mishra, George J. Pappas, Oleg Sokolsky

    EMSOFT (2001), pp. 14-31

  •  

    Hybrid Modeling and Simulation of Biomolecular Networks

    Rajeev Alur, Calin Belta, Franjo Ivancic

    HSCC (2001), pp. 19-32

  •  

    An automatic rule base generation method for fuzzy pattern recognition with multiphased clustering

    Franjo Ivancic, Ashutosh Malaviya, Liliane Peters

    KES (3) (1998), pp. 66-75