Guodong Li

US Patent:

8595701, Nov 26, 2013

Filed:

Feb 4, 2011

Appl. No.:

13/021604

Inventors:

Guodong Li - San Jose CA, US
Sreeranga P. Rajan - Sunnyvale CA, US
Indradeep Ghosh - Cupertino CA, US

Assignee:

Fujitsu Limited - Kawasaki-shi

International Classification:

G06F 9/44

US Classification:

717124, 717118, 717126, 717127

Abstract:

In particular embodiments, a method includes accessing bytecode generated by a compiler from a software program for execution by a particular processing unit; accessing configuration information describing one or more aspects of the particular processing unit; symbolically executing the bytecode with the configuration information; and, based on the symbolic execution, generating one or more results conveying a functional correctness of the software program with respect to the particular processing unit for communication to a user and generating one or more test cases for the software program for communication to a user.

US Patent:

8645924, Feb 4, 2014

Filed:

Jun 6, 2011

Appl. No.:

13/154274

Inventors:

Guodong Li - San Jose CA, US
Sreeranga P. Rajan - Sunnyvale CA, US
Indradeep Ghosh - Cupertino CA, US

Assignee:

Fujitsu Limited - Kawasaki-shi

International Classification:

G06F 9/44

US Classification:

717132, 717124, 717131, 717133, 717151, 717154, 717155, 717156

Abstract:

In one embodiment, symbolically executing a software module having a number of execution paths; and losslessly reducing the number of execution paths during the symbolic execution of the software module.

US Patent:

20120192150, Jul 26, 2012

Filed:

Jan 20, 2011

Appl. No.:

13/010714

Inventors:

Guodong LI - San Jose CA, US
Sreeranga P. RAJAN - Sunnyvale CA, US
Indradeep GHOSH - Cupertino CA, US

Assignee:

FUJITSU LIMITED - Kanagawa

International Classification:

G06F 9/44

US Classification:

717118

Abstract:

Particular embodiment compile a C++ program having one or more input variables to obtain bytecode of the C++ program; compile a C++ library to obtain bytecode of the C++ library; symbolically execute the bytecode of the C++ program and the bytecode of the C++ library, comprising assign a symbolic input to each input variable of the C++ program; determine one or more execution paths in the C++ program; and for each execution path, construct a symbolic expression that if satisfied, causes the C++ program to proceed down the execution path; and generate one or more test cases for the C++ program by solving the symbolic expressions.

US Patent:

20120192162, Jul 26, 2012

Filed:

Jan 20, 2011

Appl. No.:

13/010736

Inventors:

Guodong Li - San Jose CA, US
Sreeranga P. Rajan - Sunnyvale CA, US
Indradeep Ghosh - Cupertino CA, US

Assignee:

FUJITSU LIMITED - Kanagawa

International Classification:

G06F 9/45

US Classification:

717141, 717146

Abstract:

Particular embodiments discover a relationship between a plurality of methods of a C++ object; define one or more rules to represent the relationship; verify the rules by symbolically executing the methods; and if the rules are verified, then use the rules when symbolically executing the methods so that bytecode of the methods is not executed.

US Patent:

20120192169, Jul 26, 2012

Filed:

Jan 20, 2011

Appl. No.:

13/010691

Inventors:

Guodong Li - San Jose CA, US
Sreeranga P. Rajan - Sunnyvale CA, US
Indradeep Ghosh - Cupertino CA, US

Assignee:

FUJITSU LIMITED - Kanagawa

International Classification:

G06F 9/45

US Classification:

717161

Abstract:

Particular embodiments optimize a C++ function comprising one or more loops for symbolic execution, comprising for each loop, if there is a branching condition within the loop, then rewrite the loop to move the branching condition outside the loop. Particular embodiments may further optimize the C++ function through simplified symbolic expressions and adding constructs forcing delayed interpretation of symbolic expressions during the symbolic execution.

US Patent:

20130318503, Nov 28, 2013

Filed:

May 25, 2012

Appl. No.:

13/481594

Inventors:

Guodong Li - San Jose CA, US
Praveen K. Murthy - Fremont CA, US
Indradeep Ghosh - Cupertino CA, US
Sreeranga Rajan - Sunnyvale CA, US

Assignee:

FUJITSU LIMITED - Kanagawa

International Classification:

G06F 9/44

US Classification:

717126

Abstract:

A method includes, by one or more computing devices, determining JavaScript statements to be evaluated, parsing the JavaScript statements, translating the JavaScript statements into Java bytecodes and JavaScript-specific instructions, executing the Java bytecodes in a Java execution engine, calling a JavaScript run-time engine from the Java execution engine, handling one or more semantic operations associated with the JavaScript-specific instructions through use of the JavaScript run-time engine, and providing return values to the Java execution engine. The statements are configured for execution on a computing device. The set of Java bytecodes and JavaScript-specific instructions is configured to conduct symbolic execution of one or more portions of the JavaScript statements. The symbolic execution is configured to evaluate the JavaScript statements.

US Patent:

20130326485, Dec 5, 2013

Filed:

May 29, 2012

Appl. No.:

13/482598

Inventors:

Indradeep Ghosh - Cupertino CA, US
Guodong Li - San Jose CA, US

Assignee:

FUJITSU LIMITED - Kanagawa

International Classification:

G06F 9/44

US Classification:

717126

Abstract:

A method includes, by computing devices, analyzing numeric and string constraints associated with a software module that includes numeric and string variables and operations applying to specific variables for numeric or string results. The numeric constraints apply to specific numeric variables. The string constraints apply to specific string variables. The method further includes determining an over-approximated constraint from the numeric constraints or operations, representing the over-approximated constraint and string constraints with finite state machines, representing the numeric constraints with an equation, determining whether a solution does not exist for the combination of the variables that satisfies the over-approximated constraint, the numeric constraints, and the string constraints using operations, and terminating attempts to solve for the variables based on the determination whether the solution does not exist. The over-approximated constraint includes a superset of the numeric constraints or operations and applies to specific string variables.

US Patent:

20140047217, Feb 13, 2014

Filed:

Aug 9, 2012

Appl. No.:

13/570906

Inventors:

Guodong LI - San Jose CA, US
Indradeep GHOSH - Cupertino CA, US
Sreeranga P. RAJAN - Sunnyvale CA, US

Assignee:

FUJITSU LIMITED - Kawasaki-shi

International Classification:

G06F 9/30

US Classification:

712216, 712E09016

Abstract:

A satisfiability checking system may include a single instruction, multiple data (SIMD) machine configured to execute multiple threads in parallel. The multiple threads may be divided among multiple blocks. The SIMD machine may be further configured to perform satisfiability checking of a formula including multiple parts. The satisfiability checking may include assigning one or more of the parts to one or more threads of the multiple threads of a first block of the multiple blocks. The satisfiability checking may further include processing the assigned one or more parts in the first block such that first results are calculated based on a first proposition. The satisfiability checking may further include synchronizing the results among the one or more threads of the first block.