nec-logo

formalGrayFranjo Ivančić

Senior Research Staff Member

NEC Laboratories America

4 Independence Way, Suite 200

Princeton, NJ 08540

txp_figE-mail:

 

 

Adjunct Assistant Professor

Columbia University

Dept. of Computer Science

Fu Foundation School of Engineering and Applied Science

New York, NY 10027

 

 

I am a researcher at the NEC Labs in Princeton, where I work on software verification in the System Analysis & Verification group. Prior to joining NEC, I completed my Ph.D. in the department of Computer and Information Science at the University of Pennsylvania in Philadelphia. I was working with Professor Rajeev Alur and other colleagues at the SDRL lab. My research focused on the modeling and verification of embedded and hybrid systems.

 

Before my arrival in Philadelphia I was a Computer Science student at the Rheinische Friedrich-Wilhelms University of Bonn, Germany. I completed my studies there in June 1999 earning the Diplom-Informatiker degree. I was also working at the German National Research Center for Information Technology - GMD (now part of the Fraunhofer Institute) as a research assistant. My research there focused on Fuzzy Pattern Recognition, Handwriting Recognition and Machine Learning. Before coming to Bonn I went to high school at Quirinus-Gymnasium in my hometown of Neuss, Germany, although I am of Croatian descent.

  

Publications

2009

*      Muzaffer O. Simsir, Srihari Cadambi, Franjo Ivančić, 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), accepted for publication, 2009.

*      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.

2008

*      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.

*      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).

*      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.

2007

*      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).

2006

*      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.

2005

*      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.

2004

*      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.

2003

*      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.

*      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).

2002

*      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).

2001

*      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.

2000

*      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.

1999

*      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.

1998

*      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.

 

 

Program committee memberships:

  • 4th International Computer Science Symposium in Russia (CSR 09), August 2009.
  • 2nd International Workshop on Numerical Software Verification: Verification of Cyber-Physical Software Systems (NSV 09), April 2009.
  • 6th International Symposium on Automated Technology for Verification and Analysis (ATVA 08), October 2008.
  • 15th International SPIN Workshop on Model Checking Software (SPIN 08), August 2008.
  • International Workshop on Numerical Abstraction in Software Verification, July 2008 (co-organizer).
  • 10th Conference on Hybrid Systems: Computation and Control (HSCC 07), April 2007.
  • 6th Workshop on Compiler Optimization Meets Compiler Verification (COCV 07), March 2007.
  • 21st ACM Symposium on Applied Computing (SAC) - Software Verification Track, April 2006.

 

NEC Laboratories America Home

2009 NEC Laboratories America, Inc. All rights reserved.

 

Annual revision performed in April 2009.