Publications

2014

  • Franjo Ivančić, Gogul Balakrishnan, Aarti Gupta, Sriram Sankaranarayanan, Naoto Maeda, Takashi Imoto, Rakesh Pothengil, and Mustafa Hussain: Scalable and scope-bounded software verification in Varvel, Journal on Automated Software Engineering, Springer, August 2014. 
  • Yifei Yuan, Franjo Ivančić, Cristian Lumezanu, Shuyuan Zhang, and Aarti Gupta: Generating Consistent Updates for Software-Defined Network Configurations, ACM SIGCOMM Workshop on Hot Topics in Software Defined Networks (HotSDN), Chicago, IL, August 2014.
  • Xusheng Xiao, Gogul Balakrishnan, Franjo Ivančić, Naoto Maeda, Aarti Gupta, and Deepak Chhetri: ARC++: : Effective Typestate and Lifetime Dependency AnalysisInternational Symposium on Software Testing and Analysis (ISSTA), San Jose, CA, July 2014.
  • Abhishek Sharma, Franjo Ivančić, Alexandru Niculescu-Mizil, Haifeng Chen, Guofei Jiang: Modeling and analytics for cyber-physical systems in the age of big data. SIGMETRICS Performance Evaluation Review 41(4): 74-77 (2014).
  • Yu Lin, Franjo Ivančić, Pallavi Joshi, Gogul Balakrishnan, Malay Ganai, and Aarti Gupta: Environment-Sensitive Performance Tuning for Distributed Service OrchestrationThe Ninth International Workshop on Automatic Performance Tuning (iWAPT), Eugene, OR, June 2014.
  • Shuyuan Zhang, Franjo Ivančić, Cristian Lumezanu, Yifei Yuan, Aarti Gupta, and Sharad Malik: An Adaptable Rule Placement for Software-Defined NetworksThe 44th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), Atlanta, GA, June 2014.

2013

  • Georgios Fainekos, Sriram Sankaranarayanan, Houssam Abbas, Franjo Ivančić, and Aarti Gupta: Probabilistic Temporal Logic Falsification of Cyber-Physical SystemsACM Transactions on Embedded Computing Systems (TECS), volume 12 (2s), 2013, ACM (special issue on probabilistic embedded computing).
  • 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 DataBig 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 Execution35th International Conference on Software Engineering (ICSE), San Francisco, CA, May 2013.

2012

  • Niloofar Razavi, Franjo Ivančić, Vineet Kahlon, and Aarti Gupta: Concurrent Test Generation using Concolic Multi-Trace Analysis10th 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 Probabilities6th International Workshop on Reachability Problems (RP), Bordeaux, France, September 2012.
  • Georgios Fainekos, Eric Goubault, Franjo Ivančić, and Sriram Sankaranarayanan: Editorial: Special Section VCPSS 09ACM 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 AnalysisInternational 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 Interpretation13th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Philadelphia, PA, January 2012.

2011

  • Naoto Maeda, Takashi Imoto, Fusako Mitsuhashi, Franjo Ivančić, Gogul Balakrishnan, and Aarti Gupta: VARVEL: A Scalable Software Model CheckerIEEE 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 Verification26th 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++ Strings2nd International Conference on Formal Verification of Object-Oriented Software (FoVeOOS), Turin, Italy, October 2011. 
  • 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.

2010

  • Aarti Gupta and Franjo IvančićPrecise and scalable program analysis at NEC LabsWorkshop 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 ProblemsFormal 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 NECFormal 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 checking8th 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 CORDIC8th 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 Systems13rd 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 Programs37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL), Madrid, Spain, January 2010. (download from ACM)

2009

  • Georgios E. Fainekos, Sriram Sankaranarayanan, Franjo Ivančić, and Aarti Gupta: Robustness of Simulink Simulations30th IEEE Real-Time Systems Symposium (RTSS), Washington, DC, December 2009.
  • Franjo Ivančić, Sriram Sankaranarayanan, and Chao Wang: Foreword: Special issue on numerical software verificationFormal 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 CORDICFormal 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 AnalysisInternational Conference on Embedded Software (EMSOFT), Grenoble, France, October 2009. (download from ACM)
  • Muzaffer O. SimsirSrihari Cadambi, Franjo Ivancic, Martin Roetteler, and Niraj K. JhaA Hybrid Nano-CMOS Architecture for Defect and Fault ToleranceACM 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. ShashisharGenerating and Analyzing Symbolic Traces of Simulink/Stateflow Models21st International Conference on Computer-Aided Verification (CAV), Grenoble, France, July 2009.
  • Richard Chang, Guofei Jiang, Franjo Ivančić, Sriram Sankaranarayanan, and Vitaly ShmatikovInputs of Coma: Static Detection of Denial-of-Service Vulnerabilities22nd IEEE Computer Security Foundations Symposium (CSF22), Port Jefferson, NY, July 2009.
  • Shantanu Gupta, Florin Sultan, Srihari Cadambi, Franjo Ivančić, and Martin RoettelerUsing Hardware Transactional Memory for Data Race Detection23rd 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 AnalysisACM 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 AsharEfficient SAT-based Bounded Model Checking for Software VerificationJournal on Theoretical Computer Science (TCS), Volume 404(3), September 2008, pages 256-274, Elsevier.
  • Aleksandr ZaksZijiang Yang, Ilya Shlyakhter, Franjo IvančićSrihari Cadambi, Malay K. Ganai, Aarti Gupta, and Pranav AsharBitwidth Reduction via Symbolic Interval Analysis for Software Model CheckingTransactions 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 LearningInternational 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 Refinement15th International Static Analysis Symposium (SAS), Valencia, Spain, July 2008.
  • Shantanu Gupta, Florin Sultan, Srihari Cadambi, Franjo Ivančić, and Martin RoettelerRaceTM: Detecting Data Races using Transactional Memory20th 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 Programming30th 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 Polyhedra11th 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 Polyhedra14th 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 Software2008 Design and Verification Conference (DVCon), San Jose, CA, February 2008 (invited paper).
  • Muzaffer O. SimsirSrihari Cadambi, Franjo Ivančić, Martin Roetteler, and Niraj K. JhaFault-Tolerant Computing Using a Hybrid Nano-CMOS Architecture21st International Conference on VLSI Design, Hyderabad, India, January 2008.

2007

  • Chao Wang, Aarti Gupta, and Franjo IvančićInduction in CEGAR for Detecting Counterexamples7th 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 Sampling6th 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 Ranges14th 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 Polyhedra19th 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 VerificationACM 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 CounterexamplesFourth 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 Domains13th International Static Analysis Symposium (SAS), Seoul, Korea, August 2006.
  • Aleksandr ZaksSrihari Cadambi, Ilya Shlyakhter, Franjo IvančićZijiang Yang, Malay K. Ganai, Aarti Gupta, and Pranav AsharRange Analysis for Software VerificationInternational 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 Representations4th 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 Checking9th 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)

2005

  • Chao Wang, Aarti Gupta, Franjo Ivančić, and Malay K. Ganai: Deciding Separation Logic Formulae with SAT and Incremental Negative Cycle Elimination12th 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-SoftInternational 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 Locks17th International Conference on Computer Aided Verification (CAV), Edinburgh, UK, July 2005.
  • Franjo IvančićZijiang Yang, Malay K. Ganai, Aarti Gupta, and Pranav AsharF-Soft: Software Verification Platform17th International Conference on Computer-Aided Verification (CAV), Edinburgh, UK, July 2005.
  • Franjo IvančićModel-Based Development for Hybrid SystemsWorkshop 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 Abstraction11th 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 AsharEfficient SAT-based Bounded Model Checking for Software Verification1st International Symposium for Leveraging Applications of Formal Methods, Pathos, Cyprus, November 2004.
  • Ansgar Fehnker and Franjo IvančićBenchmarks for Hybrid Systems Verification7th International Workshop on Hybrid Systems: Computation and Control, Philadelphia, PA, March 2004.

2003

  • Franjo IvančićModeling and Analysis of Hybrid SystemsDissertation, University of Pennsylvania, Philadelphia, PA, December 2003. 
  • Rajeev Alur, Franjo IvančićJesung Kim, Insup Lee, and Oleg SokolskyGenerating Embedded Software from Hierarchical Hybrid ModelsLanguages, 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 Abstraction6th 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 Systems9th 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 SokolskyHierarchical Modeling and Analysis of Embedded SystemsProceedings 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 Navigation15th International Conference on Computer Animation, Geneva, Switzerland, June 2002.
  • Rajeev Alur, Thao Dang, and Franjo IvančićReachability Analysis of Hybrid Systems via Predicate Abstraction5th International Workshop on Hybrid Systems: Computation and Control, Stanford, California, April 2002 (LNCS 2289).
  • Eric Aaron, Franjo Ivančić, and Dimitris Metaxas: Intelligent Autonomous Agents5th International Workshop on Hybrid Systems: Computation and Control, Stanford, California, April 2002 (LNCS 2289).

2001

  • Rajeev Alur, Thao Dang, Joel Esposito, Rafael FierroYerang 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 SokolskyA 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 SchugHybrid Modeling of Biomolecular Networks4th International Workshop on Hybrid Systems: Computation and Control, Rome, Italy, April 2001 (LNCS 2034).
  • Greg Bond, Franjo Ivančić, Richard Trefler, and Nils KlarlundEclipse Feature Logic Analysis2nd 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 Clustering2nd International Conference on Knowledge-Based Intelligent Electronic Systems, Adelaide, South Australia, April 1998.