Franjo Ivancic

7693690, Apr 6, 2010

Mar 3, 2006

11/367665

Chao Wang - Plainsboro NJ, US
Aarti Gupta - Princeton NJ, US
Zijiang Yang - Northville MI, US
Franjo Ivancic - Jersey City NJ, US

NEC Laboratories America, Inc. - Princeton NJ

G06F 17/50
G06F 13/00

703 2, 703 13, 716 3, 716 5, 714 30

A symbolic disjunctive image computation method for software models which exploits a number of characteristics unique to software models. More particularly, and according to our inventive method, the entire software model is decomposed into a disjunctive set of submodules and a separate set of transition relations are constructed. An image/reachability analysis is performed wherein an original image computation is divided into a set of image computation steps that may be performed on individual submodules, independently from any others. Advantageously, our inventive method exploits variable locality during the decomposition of the original model into the submodules. By formulating this decomposition as a multi-way hypergraph partition problem, we advantageously produce a small set of submodules while simultaneously minimizing the number of live variable in each individual submodule. Our inventive method produces a set of disjunctive transition relations directly from the software model, without producing a conjunctive transition relation—as is necessary in the prior art. In addition, our inventive method exploits the exclusive use of live variables in addition to novel search strategies which provide still further benefit to our method.

7930659, Apr 19, 2011

Jun 3, 2006

11/422069

Franjo Ivancic - Jersey City NJ, US
Aarti Gupta - Princeton NJ, US
Malay Ganai - Plainsboro NJ, US
Himanshu Jain - Pittsburgh PA, US

NEC Laboratories America, Inc. - Princeton NJ

G06F 17/50

716100

A system and method is disclosed for formal verification of software programs that advantageously improves performance of an abstraction-refinement loop in the verification system.

8006239, Aug 23, 2011

Jan 16, 2008

12/015126

Sriram Sankaranarayanan - Plainsboro NJ, US
Aarti Gupta - Princeton NJ, US
Franjo Ivancic - Jersey City NJ, US
Ilya Shlyakhter - Franklin Park NJ, US

NEC Laboratories America, Inc. - Princeton NJ

G06F 9/44
G06F 9/45

717154, 717124, 717131, 717151

A computer implemented method for generating a representation of relationships between variables in a program employing Symbolic Range Constraints (SRCs) wherein the SRCs are of the form φ:^l≦x≦uwhere for each i ε[l,n], the linear expressions l,uare made up of variables in the set{x,. . . ,x} and wherein the SRCs comprise linear, convex, and triangulated constraints for a given variable order.

8126831, Feb 28, 2012

Sep 23, 2008

12/236102

Sriram Sankaranarayanan - Plainsboro NJ, US
Franjo Ivancic - Princeton NJ, US
Aarti Gupta - Princeton NJ, US

NEC Laboratories America, Inc. - Princeton NJ

G06N 5/00

706 45

A system and method for inferring preconditions for procedures in a program includes formulating predicates based on inputs to a procedure, including formal arguments, global variables and external environment. Truth assignments are sampled to the predicates to provide truth assignments that lead to a feasible set of input values. Test cases are generated for testing the program in accordance with the truth assignments having feasible sets of input values. The truth assignments are classified to the predicates as providing an error or not providing an error.

8131532, Mar 6, 2012

Jun 3, 2006

11/422068

Srihari Cadambi - Cherry Hill NJ, US
Aleksandr Zaks - Brooklyn NY, US
Franjo Ivancic - Jersey City NJ, US
Ilya Shlyakhter - Franklin Park NJ, US
Zijiang Yang - Northville MI, US
Malay Ganai - Plainsboro NJ, US
Aarti Gupta - Princeton NJ, US
Pranav Ashar - Belle Mead NJ, US

NEC Laboratories America, Inc. - Princeton NJ

G06F 9/45
G06F 9/44
G06F 9/455

703 22, 717126, 703 26

A system and method is disclosed for formal verification of software programs that advantageously bounds the ranges of values that a variable in the software can take during runtime.

8191045, May 29, 2012

Mar 18, 2008

12/050624

Sriram Sankaranarayanan - Plainsboro NJ, US
Franjo Ivancic - Jersey City NJ, US
Aarti Gupta - Princeton NJ, US

NEC Laboratories America, Inc. - Princeton NJ

G06F 9/44
G06F 9/445

717124, 717127, 717129

A system and method for mining program specifications includes generating unit tests to exercise functions of a library through an application program interface (API), based upon an (API) signature. A response to the unit tests is determined to generate a transaction in accordance with a target behavior. The transaction is converted into a relational form, and specifications of the library are learned using an inductive logic programming tool from the relational form of the transaction.

8352222, Jan 8, 2013

Sep 23, 2008

12/236071

Sriram Sankaranarayanan - Plainsboro NJ, US
Franjo Ivancic - Princeton NJ, US

NEC Laboratories America, Inc. - Princeton NJ

G06F 17/10
G06F 7/60
G06F 7/00
H03K 3/00
G06G 7/00
G06E 3/00

703 2, 327199, 708800, 708821, 708854

In accordance with aspects of the present principles, an over-approximation of reachable states of a hybrid system may be determined by utilizing template polyhedra. Policy iteration may be utilized to obtain an over-approximation of reachable states in the form of a relaxed invariant based upon template polyhedra expressions. The relaxed invariant may be used to construct a flowpipe to refine the over-approximation and thereby determine the reachable states of the hybrid system.

8365152, Jan 29, 2013

Jul 31, 2008

12/183416

Gogul Balakrishnan - Plainsboro NJ, US
Sriram Sankaranarayanan - Plainsboro NJ, US
Franjo Ivancic - Princeton NJ, US
Aarti Gupta - Princeton NJ, US

NEC Laboratories America, Inc. - Princeton NJ

G06F 9/45

717138, 717152

A system and method for infeasible path detection includes performing a static analysis on a program to prove a property of the program. If the property is not proved, infeasible paths in the program are determined by performing a path-insensitive abstract interpretation. Information about such infeasible paths is used to achieve the effects of path-sensitivity in path-insensitive program analysis.