
Franjo Ivančić
Senior Research Staff
Member
Adjunct Assistant Professor
Dept. of Computer Science
Fu Foundation
I am a researcher at the NEC
Labs in
Before my arrival in
Abhishek Sharma, Franjo Ivančić,
Alexandru Niculescu-Mizil, Haifeng Chen, and Guofei Jiang: Modeling
and Analytics for Cyber-Physical Systems in the Age of Big Data, Big Data Analytics Workshop (BDAW),
Pittsburgh, PA, June 2013.
Pranav Garg, Franjo Ivančić,
Gogul Balakrishnan, Naoto Maeda, and Aarti Gupta: Feedback-Directed Unit Test Generation for C/C++ using Concolic
Execution, 35th International
Conference on Software Engineering (ICSE), San Francisco, CA, May 2013.
Georgios Fainekos, Sriram Sankaranarayanan, Houssam Abbas, Franjo Ivančić,
and Aarti Gupta: Probabilistic Temporal Logic
Falsification of Cyber-Physical Systems, ACM Transactions on Embedded Computing Systems (TECS), accepted for
publication, ACM (special issue on
probabilistic embedded computing).
Niloofar Razavi, Franjo Ivančić,
Vineet Kahlon, and Aarti Gupta: Concurrent
Test Generation using Concolic Multi-Trace Analysis, 10th Asian Symposium on Programming Languages and Systems (APLAS),
Kyoto, Japan, December 2012.
Khalil Ghorbal, Parasara Sridhar Duggirala,
Vineet Kahlon, Franjo Ivančić, and Aarti
Gupta: Efficient Probabilistic Model Checking of Systems with Ranged
Probabilities, 6th International Workshop on Reachability Problems (RP),
Bordeaux, France, September 2012.
Georgios
Fainekos, Eric Goubault, Franjo Ivančić,
and Sriram Sankaranarayanan: Editorial: Special
Section VCPSS 09, ACM Transactions on
Embedded Computing Systems (TECS), volume 11, issue S2, August 2012, ACM (forward to special issue).
Jing Yang, Gogul Balakrishnan, Naoto Maeda,
Franjo Ivančić, Aarti Gupta, Nishant Sinha, Sriram
Sankaranarayanan, and Naveen Sharma: Object Model Construction for
Inheritance in C++ and its Applications to Program Analysis, International
Conference on Compiler Construction (CC), Tallinn, Estonia, March 2012.
Khalil Ghorbal, Franjo Ivančić,
Gogul Balakrishnan, Naoto Maeda, and Aarti Gupta: Donut Domains:
Efficient Non-Convex Domains for Abstract Interpretation, 13th
International Conference on Verification, Model Checking, and Abstract
Interpretation (VMCAI), Philadelphia, PA, January 2012.
Naoto Maeda, Takashi Imoto, Fusako
Mitsuhashi, Franjo Ivančić,
Gogul Balakrishnan, and Aarti Gupta: VARVEL: A Scalable Software Model
Checker, IEEE 22nd International Symposium on Software Reliability
Engineering (ISSRE), Hiroshima, Japan, November 2011 (track on
industrial practices).
Franjo Ivančić,
Gogul Balakrishnan, Aarti Gupta, Sriram Sankaranarayanan, Naoto Maeda, Hiroki Tokuoka, Takashi Imoto, and Yoshiaki Miyazaki: DC2:
A Framework for Scalable, Scope-Bounded Software Verification, 26th
IEEE/ACM International Conference on Automated Software Engineering (ASE),
Lawrence, KS, November 2011.
Gogul Balakrishnan, Naoto Maeda, Sriram
Sankaranarayanan, Franjo Ivančić, Aarti
Gupta and Rakesh Pothengil:
Modeling and Analyzing the Interaction of C and C++ Strings, 2nd
International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Turin, Italy, October 2011. [Pre-proceedings
version, as included in Technical Report,
Dept. of Informatics, Karlsruhe Institute of Technology, 2011-26: PDF]
Prakash Prabhu, Naoto Maeda, Gogul Balakrishnan, Franjo Ivančić, and Aarti Gupta: Interprocedural
Exception Analysis for C++, 25th European Conference on
Object-Oriented Programming (ECOOP), Lancaster, UK, July 2011.
Aarti Gupta and Franjo Ivančić:
Precise and scalable program analysis at NEC Labs, Workshop
on Usable Verification, Redmond, WA, November 2010 (invited paper).
Sicun Gao, Malay K. Ganai, Franjo Ivančić, Aarti Gupta, Sriram Sankaranarayanan,
and Edmund M. Clarke: Integrating ICP and LRA Solvers for Deciding
Nonlinear Real Arithmetic Problems, Formal Methods in Computer
Aided Design (FMCAD), Lugano, Switzerland,
October 2010.
Gogul Balakrishnan, Malay K. Ganai, Aarti Gupta,
Franjo Ivančić, Vineet Kahlon, Weihong Li, Naoto Maeda, Nadia Papakonstantinou,
Sriram Sankaranarayanan, Nishant Sinha,
and Chao Wang: Scalable and precise program analysis at NEC, Formal
Methods in Computer Aided Design (FMCAD), Lugano,
Switzerland, October 2010 (invited paper).
Franjo Ivančić,
Malay K. Ganai, Sriram Sankaranarayanan, and Aarti Gupta: Numerical
stability analysis of floating-point computations using software model checking,
8th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), Grenoble, France, July 2010.
Malay K. Ganai and Franjo Ivančić:
Efficient Decision Procedure for Non-linear Arithmetic Constraints
using CORDIC, 8th International Workshop on Satisifiability
Modulo Theories (SMT), Edinburgh, UK, July 2010 (presentation only submission).
Truong X. Nghiem,
Sriram Sankaranarayanan, Georgios Fainekos, Franjo Ivančić,
Aarti Gupta and George J. Pappas: Monte-Carlo Techniques for
Falsification of Temporal Properties of Non-Linear Systems, 13rd International
Conference on Hybrid Systems: Computation and Control (HSCC), Stockholm,
Sweden, April 2010. (download
from ACM)
William R. Harris, Sriram Sankaranarayanan,
Franjo Ivančić, and Aarti Gupta: Program
Analysis via Satisfiability Modulo Path Programs,
37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages
(POPL), Madrid, Spain, January 2010. (download from ACM)
Georgios E. Fainekos, Sriram Sankaranarayanan,
Franjo Ivančić, and Aarti Gupta: Robustness
of Simulink Simulations, 30th IEEE Real-Time Systems Symposium
(RTSS), Washington, DC, December 2009.
Franjo Ivančić,
Sriram Sankaranarayanan, and Chao Wang: Foreword: Special issue on
numerical software verification, Formal Methods in System Design
(FMSD), volume 35(3), December 2009, Springer (foreword to special
issue).
Malay K. Ganai and Franjo Ivančić:
Efficient Decision Procedure for Non-linear Arithmetic Constraints
using CORDIC, Formal Methods in Computer Aided Design (FMCAD),
Austin, TX, November 2009.
Gogul Balakrishnan, Sriram Sankaranarayanan,
Franjo Ivančić, and Aarti Gupta: Refining
the Control Structure of Loops using Static Analysis, International
Conference on Embedded Software (EMSOFT), Grenoble, France, October 2009. (download from ACM)
Muzaffer O. Simsir, Srihari Cadambi, Franjo
Ivancic, Martin Roetteler, and Niraj
K. Jha: A Hybrid Nano-CMOS Architecture for
Defect and Fault Tolerance, ACM Journal on Emerging Technologies
in Computing Systems (JETC), volume 5(3), August 2009, ACM.
Aditya Kanade, Rajeev Alur, Franjo Ivančić,
S. Ramesh, Sriram Sankaranarayanan and K.C. Shashishar:
Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models, 21st International
Conference on Computer-Aided Verification (CAV), Grenoble, France, July
2009.
Richard Chang, Guofei
Jiang, Franjo Ivančić, Sriram
Sankaranarayanan, and Vitaly Shmatikov:
Inputs of Coma: Static Detection of Denial-of-Service Vulnerabilities,
22nd IEEE Computer Security Foundations Symposium (CSF22), Port
Jefferson, NY, July 2009.
Shantanu Gupta, Florin
Sultan, Srihari Cadambi, Franjo Ivančić,
and Martin Roetteler: Using Hardware
Transactional Memory for Data Race Detection, 23rd IEEE
International Parallel and Distributed Processing Symposium (IPDPS), Rome,
Italy, May 2009.
Zijiang Yang, Chao
Wang, Aarti Gupta and Franjo Ivančić: Model
Checking Sequential Software Programs via Mixed Symbolic Analysis, ACM Transactions on Design Automation of
Electronic Systems (TODAES), volume 13(1), January 2009, ACM.
Franjo Ivančić,
Zijiang Yang, Malay K. Ganai, Aarti Gupta, and Pranav
Ashar: Efficient SAT-based Bounded Model
Checking for Software Verification, Journal on Theoretical
Computer Science (TCS), Volume 404(3), September 2008, pages 256-274,
Elsevier.
Aleksandr Zaks, Zijiang Yang, Ilya Shlyakhter, Franjo Ivančić, Srihari
Cadambi, Malay K. Ganai, Aarti Gupta, and Pranav Ashar:
Bitwidth Reduction via
Symbolic Interval Analysis for Software Model Checking, Transactions
Brief Paper in the IEEE Transactions on CAD, volume 27(8), Aug. 2008,
pages 1513-1517, IEEE.
Sriram Sankaranarayanan, Swarat Chaudhuri,
Franjo Ivančić, and Aarti Gupta: Dynamically
Inferring Likely Data Preconditions over Predicates by Tree Learning, International
Symposium on Software Testing and Analysis (ISSTA), Seattle, WA, July
2008. (download
from ACM)
Gogul Balakrishnan, Sriram Sankaranarayanan,
Franjo Ivančić, Ou
Wei, and Aarti Gupta: SLR: Path-Sensitive Analysis through
Infeasible-Path Detection and Syntactic Language Refinement, 15th
International Static Analysis Symposium (SAS), Valencia, Spain, July 2008.
Shantanu Gupta, Florin
Sultan, Srihari Cadambi, Franjo Ivančić,
and Martin Roetteler: RaceTM:
Detecting Data Races using Transactional Memory, 20th ACM
Symposium on Parallelism in Algorithms and Architectures (SPAA), Munich, Germany,
June 2008 (short paper). (download from ACM)
Sriram Sankaranarayanan, Franjo Ivančić, and Aarti Gupta: Mining Library
Specifications using Inductive Logic Programming, 30th
International Conference on Software Engineering (ICSE), Leipzig, Germany,
May 2008.
Sriram Sankaranarayanan, Thao
Dang, and Franjo Ivančić: A Policy
Iteration Technique for Time Elapse over Template Polyhedra,
11th International Conference on Hybrid Systems: Computation and Control
(HSCC), St. Louis, MO, April 2008 (short
paper).
Sriram Sankaranarayanan, Thao
Dang, and Franjo Ivančić: Symbolic
Model Checking of Hybrid Systems using Template Polyhedra,
14th International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS), Budapest, Hungary, April 2008.
Malay K. Ganai, Aarti Gupta, Franjo Ivančić, Vineet Kahlon, Weihong
Li, Nadia Papakonstantinou, Sriram Sankaranarayanan,
and Chao Wang: Towards Precise and Scalable Verification of Embedded
Software, 2008 Design and Verification Conference (DVCon), San Jose, CA, February 2008 (invited paper).
Muzaffer O. Simsir, Srihari Cadambi, Franjo Ivančić, Martin Roetteler,
and Niraj K. Jha: Fault-Tolerant
Computing Using a Hybrid Nano-CMOS Architecture, 21st
International Conference on VLSI Design, Hyderabad, India, January 2008.
Chao Wang, Aarti Gupta, and Franjo Ivančić: Induction in CEGAR for Detecting
Counterexamples, 7th International Conference on Formal Methods in
Computer-Aided Design (FMCAD), Austin, TX, November 2007.
Sriram Sankaranarayanan, Richard Chang, Guofei Jiang, and Franjo Ivančić:
State Space Exploration using Feedback Constraint Generation and
Monte-Carlo Sampling, 6th joint meeting of the European Software
Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of
Software Engineering (ESEC/FSE), Dubrovnik, Croatia, September 2007.
Sriram Sankaranarayanan, Franjo Ivančić, and Aarti Gupta: Program
Analysis using Symbolic Ranges, 14th International Static Analysis
Symposium (SAS), Kongens Lyngby,
Denmark, August 2007.
Chao Wang, Zijiang
Yang, Aarti Gupta and Franjo Ivančić: Using
Counterexamples for Improving the Precision of Reachability Computation with Polyhedra, 19th International Conference on
Computer-Aided Verification (CAV), Berlin, Germany, July 2007.
Chao Wang, Zijiang
Yang, Franjo Ivančić, and Aarti Gupta: Disjunctive Image Computation for Software
Verification, ACM Transactions on
Design Automation of Electronic Systems (TODAES), volume 12(2), April 2007,
article 10, ACM (received The ACM
Transaction on Design Automation of Electronic Systems (TODAES) 2008 Best Paper
Award).
Chao Wang, Zijiang
Yang, Franjo Ivančić, and Aarti Gupta: Whodunit?
Causal Analysis of Counterexamples, Fourth International Symposium
on Automated Technology for Verification and Analysis (ATVA), Beijing,
China, October 2006.
Sriram Sankaranarayanan, Franjo Ivančić, Ilya Shlyahkter, and Aarti Gupta: Static Analysis in
Disjunctive Numerical Domains, 13th International Static Analysis
Symposium (SAS), Seoul, Korea, August 2006.
Aleksandr Zaks, Srihari Cadambi, Ilya Shlyakhter, Franjo Ivančić, Zijiang Yang,
Malay K. Ganai, Aarti Gupta, and Pranav Ashar: Range
Analysis for Software Verification, International Workshop on
Software Verification and Validation (SVV), Seattle, WA, August 2006.
Himanshu Jain, Franjo Ivančić,
Ilya Shlyakhter, Chao Wang,
and Aarti Gupta: Using Statically
Computed Invariants inside the Predicate Abstraction and Refinement Loop, 18th International Conference on
Computer-Aided Verification (CAV), Seattle, WA, August 2006.
Zijiang Yang, Chao
Wang, Aarti Gupta, and Franjo Ivančić: Model
Checking C Programs using Mixed Symbolic Representations, 4th
ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), Napa Valley, CA, July 2006.
Rajeev Alur, Thao
Dang, and Franjo Ivančić: Counterexample-Guided
Predicate Abstraction of Hybrid Systems, in Journal on Theoretical
Computer Science (TCS), volume 354,
March 2006, pages 250 - 271, Elsevier.
Chao Wang, Zijiang
Yang, Franjo Ivančić, and Aarti Gupta: Disjunctive
Image Computation for Embedded Software Model Checking, 9th
International Conference on Design, Automation, and Test in Europe (DATE),
Munich, Germany, March 2006.
Rajeev Alur, Thao
Dang, and Franjo Ivančić: Predicate
Abstraction for Reachability Analysis of Hybrid Systems, in Transactions
on Embedded Computing Systems (TECS), volume 5(1), February 2006, pages
152 - 199, ACM. (download
from ACM)
Chao Wang, Aarti Gupta, Franjo Ivančić, and Malay K. Ganai: Deciding
Separation Logic Formulae with SAT and Incremental Negative Cycle Elimination,
12th International Conference on Logic for Programming Artificial
Intelligence and Reasoning (LPAR), Montego Bay, Jamaica, December 2005.
Franjo Ivančić,
Ilya Shlyakhter, Aarti
Gupta, Malay K. Ganai, Vineet Kahlon, Chao Wang, Zijiang
Yang: Model Checking C Programs Using F-Soft, International
Conference on Computer Design (ICCD), San Jose, CA, October 2005 (invited paper).
Vineet Kahlon, Franjo Ivančić,
and Aarti Gupta: Reasoning about Threads Communicating via Locks,
17th International Conference on Computer Aided Verification (CAV),
Edinburgh, UK, July 2005.
Franjo Ivančić,
Zijiang Yang, Malay K. Ganai, Aarti Gupta, and Pranav
Ashar: F-Soft: Software Verification Platform,
17th International Conference on Computer-Aided Verification (CAV),
Edinburgh, UK, July 2005.
Franjo Ivančić:
Model-Based Development for Hybrid Systems, Workshop on
Model-Based Development and Testing, Orlando, FL, July 2005.
Himanshu Jain, Franjo Ivančić,
Malay K. Ganai, and Aarti Gupta: Localization and Register Sharing for
Predicate Abstraction, 11th International Conference on Tools and
Algorithms for the Construction and Analysis of Systems (TACAS),
Edinburgh, UK, April 2005.
Franjo Ivančić,
Zijiang Yang, Aarti Gupta, Malay K. Ganai, and Pranav
Ashar: Efficient SAT-based Bounded Model Checking
for Software Verification, 1st International Symposium for Leveraging
Applications of Formal Methods, Pathos, Cyprus, November 2004.
Ansgar Fehnker and Franjo Ivančić:
Benchmarks for Hybrid Systems Verification, 7th International Workshop
on Hybrid Systems: Computation and Control, Philadelphia, PA, March 2004.
Franjo Ivančić:
Modeling and Analysis of Hybrid Systems, Dissertation, University of
Pennsylvania, Philadelphia, PA, December 2003. Dissertation abstract
Rajeev Alur, Franjo Ivančić,
Jesung Kim, Insup Lee, and
Oleg Sokolsky: Generating Embedded Software from
Hierarchical Hybrid Models, Languages, Compilers, and Tools for Embedded
Systems, San Diego, CA, June 2003. (download from ACM)
Rajeev Alur, Thao Dang
and Franjo Ivančić: Progress on
Reachability Analysis of Hybrid Systems using Predicate Abstraction, 6th
International Workshop on Hybrid Systems: Computation and Control, Prague,
Czech Republic, April 2003.
Rajeev Alur, Thao Dang
and Franjo Ivančić: Counter-Example
Guided Predicate Abstraction of Hybrid Systems, 9th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems,
Warsaw, Poland, April 2003.
Rajeev Alur, Thao
Dang, Joel Esposito, Yerang Hur,
Franjo Ivančić, Vijay Kumar, Insup Lee, Pradyumna Mishra,
George Pappas, and Oleg Sokolsky: Hierarchical
Modeling and Analysis of Embedded Systems, Proceedings of the IEEE,
(Volume 91, Number 1), January 2003 (invited
paper).
Rajeev Alur, Calin Belta, Franjo Ivančić, Vijay Kumar, Harvey Rubin, Jonathan Schug, and Jonathan Web: Visual Programming for Modeling
and Simulation of Biomolecular Networks, 9th
International Conference on High Performance Computing, Bangalore, India,
December 2002.
Eric Aaron, Harold Sun, Franjo Ivančić, and Dimitris
Metaxas: A Hybrid Dynamical Systems Approach to Intelligent Low-Level
Navigation, 15th International Conference on Computer Animation,
Geneva, Switzerland, June 2002.
Rajeev Alur, Thao
Dang, and Franjo Ivančić: Reachability
Analysis of Hybrid Systems via Predicate Abstraction, 5th International
Workshop on Hybrid Systems: Computation and Control, Stanford, California,
April 2002 (LNCS 2289).
Eric Aaron, Franjo Ivančić,
and Dimitris Metaxas: Intelligent Autonomous
Agents, 5th International Workshop on Hybrid Systems: Computation and
Control, Stanford, California, April 2002 (LNCS 2289).
Rajeev Alur, Thao
Dang, Joel Esposito, Rafael Fierro, Yerang Hur, Franjo Ivančić, Vijay Kumar, Insup
Lee, Pradyumna Mishra, George Pappas, and Oleg Sokolsky: Hierarchical Hybrid Modeling of Embedded
Systems, 1st International Workshop on Embedded Software, Tahoe
City, California, Oct. 2001 (LNCS 2211), (invited
paper).
Eric Aaron, Franjo Ivančić,
Dimitris Metaxas, and Oleg Sokolsky:
A Framework for Reasoning about Animation Systems, 3rd International
Workshop on Intelligent Virtual Agents, Madrid, Spain, Sept. 2001.
Rajeev Alur, Calin Belta, Franjo Ivančić, Vijay Kumar, Max Mintz,
George Pappas, Harvey Rubin, and Jonathan Schug: Hybrid
Modeling of Biomolecular Networks, 4th
International Workshop on Hybrid Systems: Computation and Control, Rome,
Italy, April 2001 (LNCS 2034).
Greg Bond, Franjo Ivančić,
Richard Trefler, and Nils Klarlund:
Eclipse Feature Logic Analysis, 2nd International IP-Tel, New
York City, NY, April 2001.
Franjo Ivančić,
and Liliane Peters: An Automatic Fuzzy Rule
Generation Method for Handwriting Recognition, in Encyclopedia of
Microcomputers, (Volume 26, Supplement 5), Oct. 2000.
Jaya Balasubramaniam, Franjo Ivančić,
Ashutosh Malaviya, and Liliane Peters: Handwriting Recognition with Context
Dependent Fuzzy Rules, in Knowledge-Based Intelligent Techniques in
Character Recognition (editors B. Lazzarini and
L.C. Jain), April 1999.
Franjo Ivančić:
Lernen von Regelmengen
zur Fuzzy-Mustererkennung durch mehrphasige Clusteranalyse (Learning of Sets of Rules for Fuzzy
Pattern Recognition through Multi-Phased Clustering), Diplom
Thesis, GMD Research Report No. 7/1999, Jan. 1999.
Franjo Ivančić,
Ashutosh Malaviya and Liliane Peters: An Automatic Rule-Base Generation Method
for Fuzzy Pattern Recognition with Multi-Phased Clustering, 2nd
International Conference on Knowledge-Based Intelligent Electronic Systems,
Adelaide, South Australia, April 1998.
Conference Chair:
Invited talks:
Program committee memberships:
Systems Analysis and Verification, SAV Benchmarks, Bug Gallery, NEC Laboratories America Home