Gogul A Balakrishnan

8402440, Mar 19, 2013

Feb 26, 2009

12/393500

Sriram Sankaranarayanan - Plainsboro NJ, US
Franjo Ivancic - Princeton NJ, US
William R Harris - Madison WI, US
Aarti Gupta - Princeton NJ, US
Gogul Balakrishnan - Plainsboro NJ, US

NEC Laboratories America, Inc. - Princeton NJ

G06F 9/44

717126, 717124, 717130, 717131

Systems and methods are disclosed to verify a program by symbolically enumerating path programs; verifying each path program to determine if the path program is correct or leads to a violation of a correctness property; determining a conflict set from the path program if the path program is proved correct; using the conflict set to avoid enumerating other related path programs that are also correct.

8522226, Aug 27, 2013

Feb 8, 2010

12/701962

Sriram Sankaranarayanan - Boulder CO, US
Aarti Gupta - Princeton NJ, US
Gogul Balakrishnan - Plainsboro NJ, US

NEC Laboratories America, Inc. - Princeton NJ

G06F 9/45
G06F 9/44
G06F 9/445

717160, 717150, 717151, 717167, 717171, 717178

A system and method for discovering a set of possible iteration sequences for a given loop in a software program is described, to transform the loop representation. In a program containing a loop, the loop is partitioned into a plurality of portions based on splitting criteria. Labels are associated with the portions, and an initial loop automaton is constructed that represents the loop iterations as a regular language over the labels corresponding to the portions in the program. Subsequences of the labels are analyzed to determine infeasibility of the subsequences permitted in the automaton. The automaton is refined by removing all infeasible subsequences to discover a set of possible iteration sequences in the loop. The resulting loop automaton is used in a subsequent program verification or analysis technique to find violations of correctness properties in programs.

8601459, Dec 3, 2013

Apr 9, 2013

13/859010

Aarti Gupta - Princeton NJ, US
Gogul Balakrishnan - Plainsboro NJ, US

NEC Laboratories America, Inc. - Princeton NJ

G06F 9/45
G06F 9/44

717160, 717150, 717151, 717167, 717170, 717178

A system and method for discovering a set of possible iteration sequences for a given loop in a software program is described, to transform the loop representation. In a program containing a loop, the loop is partitioned into a plurality of portions based on splitting criteria. Labels are associated with the portions, and an initial loop automaton is constructed that represents the loop iterations as a regular language over the labels corresponding to the portions in the program. Subsequences of the labels are analyzed to determine infeasibility of the subsequences permitted in the automaton. The automaton is refined by removing all infeasible subsequences to discover a set of possible iteration sequences in the loop. The resulting loop automaton is used in a subsequent program verification or analysis technique to find violations of correctness properties in programs.

20090193401, Jul 30, 2009

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

717144

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.

20090292941, Nov 26, 2009

Dec 9, 2008

12/331243

Malay K. Ganai - Plainsboro NJ, US
Gogul Balakrishnan - Plainsboro NJ, US

NEC LABORATORIES AMERICA, INC. - Princeton NJ

G06F 11/07

714 2, 714E11023

Systems and methods are disclosed for performing error diagnosis of software errors in a program by from one or more error traces, building a repair program containing one or more modified program semantics corresponding to fixes to observed errors; encoding the repair program with constraints, biases and priortization into a constraint weighted problem; and solving the constraint weighted problem to generate one or more repair solutions, wherein the encoding includes at least one of: a) constraining one or more repairs choices guided by automatically inferring one or more partial specifications of intended program behaviors and program structure; b) biasing one or more repair choices guided by typical programming mistakes; and c) prioritizing the repair solutions based on error locations and possible changes in program semantics.

20120084761, Apr 5, 2012

Sep 30, 2011

13/249298

Naoto Maeda - Tokyo, JP
Prakash Prabhu - Princeton NJ, US
Gogul Balakrishnan - Princeton NJ, US
Franjo Ivancic - Princeton NJ, US
Aarti Gupta - Princeton NJ, US

NEC LABORATORIES AMERICA, INC. - Princeton NJ

G06F 9/44

717132

An interprocedural exception analysis and transformation framework for computer programming languages such as C++ that (1) captures the control-flow induced by exceptions precisely, and (2) transforms the given computer program into an exception-free program that is amenable for precise static analysis, verification, and optimizations.

20120117547, May 10, 2012

Oct 3, 2011

13/251463

GOGUL BALAKRISHNAN - Princeton NJ, US
Naoto Maeda - Lawrenceville NJ, US
Franjo Ivancic - Princeton NJ, US
Nishant Sinha - Plainsboro NJ, US
Aarti Gupta - Princeton NJ, US
Jing Yang - Chartottesville VA, US

NEC Laboratories America, Inc. - Princeton NJ

G06F 9/45

717136

A model is provided for transforming a program with a priori given class hierarchy that is induced by inheritance. An inheritance remover is configured to remove inheritance from a given program to produce an analysis-friendly program which does not include virtual-function pointer tables and runtime libraries associated with inheritance-related operations. The analysis-friendly program preserves the semantics of the given program with respect to a given class hierarchy. A clarifier is configured to identify implicit expressions and function calls and transform the given program into at least one intermediate program having explicit expressions and function calls.

20120233584, Sep 13, 2012

Mar 9, 2012

13/416358

Franjo Ivancic - Princeton NJ, US
Gogul Balakrishnan - Princeton NJ, US
Naoto Maeda - Tokyo, JP
Aarti Gupta - Princeton NJ, US

NEC LABORATORIES AMERICA, INC. - Princeton NJ

G06F 9/44

717104

A computer implemented method for analyzing a computer software program comprising both C++ and C string components, wherein the method includes building a memory model abstraction of any memory used by the program strings. Various memory models are presented that find invalid memory accesses in terms of validity of memory regions and buffer overflows. The model supports analyzing the interaction of C and C++ components—in particular, it focuses on the interaction of C and C++ strings. The conversion of C++ strings to C strings is accomplished through a non-transferable ownership attribute that is to be respected by the C strings. The models can then be analyzed using static analysis techniques such as abstract interpretation and model checking, or through dynamic analysis. In so doing we allow discovery of potential memory safety violations in programs involving conversions between C and C++ strings.