Fujitsu Corporation

Lsi Logic Corporation

Sreeranga P Rajan

Indradeep Ghosh

Mukul Ranjan Prasad

Guodong Li

Oksana Tkachuk

Praveen Murthy

Carlos Dangelo

Vijay K Nagasamy

Ahsan Bootehsaz

Koichiro Takayama

Fangqi Sun

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.

Satisfiability checking

In one embodiment, a method may include symbolically executing application code on a first framework. The method may also include creating a first model based on the symbolic execution of the first framework. The method may additionally include symbolically executing the application code on a second framework. The method may further include creating a second model based on the symbolic execution of the first framework. The method may also include determining one or more parameters associated with the first framework based on the first model. The method may additionally include determining one or more parameters associated with the second framework based on the second model. The method may also include selecting one of the first framework and the second framework as a desired framework for execution of the application code based on a comparison of the one or more parameters associated with the first framework and the one or more parameters associated with the second framework.

System and method for comparing software frameworks

In one embodiment, a method includes accessing one or more document object model (DOM) representations of one or more pages of a Web application that comprises one or more instances of a web-application artifact. For each of one or more of the instances, the method also includes identifying a first set of one or more DOM elements in one of the DOM representations of one of the pages that collectively correspond to the instance. The method additionally includes identifying a second set of one or more particular values of one or more particular attributes of one or more particular ones of the DOM elements in the first sets. The second set may then be mapped to the web-application artifact to provide a DOM definition of the web-application artifact.

Facilitating automated validation of a web application

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.

Symbolic execution and automatic test case generation for JavaScript programs

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.

Optimizing libraries for validating C++ programs using symbolic execution

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.

Software architecture for validating C++ programs using symbolic execution

A method includes, by one or more computing devices, determining code-under-test configured for execution on a computing device to be evaluated, creating a plurality of test cases based on the symbolic execution and including a plurality of constraints, selectively conducting abstract interpretation on the constraints, selectively conducting Satisfiability Modulo Theory ('SMT') solving on the constraints, and validating or invalidating the code-under-test based on at least the SMT solving and the abstract interpretation. The abstract interpretation includes using a plurality of abstract interpretation models based on the constraints of the test case and over-approximating the constraints of the test case.

Abstract symbolic execution for scaling symbolic execution generation and automatic test generation

In one embodiment, accessing a control flow graph (CFG) of a software program written in JavaScript; identifying one or more paths in the CFG; and performing symbolic execution on the software program using the CFG.

Symbolic execution of javascript software using a control flow graph

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.

Lossless path reduction for efficient symbolic execution and automatic test generation

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.

Symbolic execution and test generation for GPU programs

A method includes accessing a page of Web application that includes an interactive form having at least one field for entry of data, the interactive form rendered by the Web application based on code for the interactive form. The method also includes extracting input validation code from the code, the input validation code including at least one constraint on data entered into the at least one field. The method additionally includes extracting the at least one constraint based on an analysis of the input validation code and solving, for the at least one field, for a string value based at least on the at least one constraint for the at least one field. The also includes automatically entering, into the at least one field, the string value. The method additionally includes automatically submitting the interactive form, including the string value entered into the at least one field.

Methods and systems for test automation of forms in web applications

In particular embodiments, an environment for modular software analysis is generated for a software module under analysis. Irrelevancy analysis is performed on the software module to determine that, for each input datum to the software module, whether the input datum is relevant or irrelevant with respect to branch coverage of the module code. A default concrete value is assigned to each irrelevant input datum. A set of concrete values is calculated for each relevant input datum using symbolic execution. The environment is enhanced such that default concrete values are passed to the software module for the irrelevant input data and sets of concrete values generated using symbolic execution are passed to the software module for the relevant input data. The enhanced environment enables module analysis with as much as 100% branch coverage of the module code.

Environment data refinement based on static analysis and symbolic execution

In one embodiment, analyze client-tier source code of a client-server software application to extract one or more software modules that handle user-input data of the software application. For each one of the software modules, extract from the software module one or more user-input constraints placed on the user-input data, comprising: analyze source code of the software module to determine one or more failure points in the source code; perform symbolic execution on the software module to extract one or more first expressions that cause the software module to reach the failure points, respectively; obtain a second expression as the disjunction of all the first expressions; obtain a third expression as the negation of the second expression; and extract the user-input constraints from the third expression. Determine one or more user-input data that satisfy all the user-input constraints.

Generating software application user-input data through analysis of client-tier source code

In one embodiment, a method includes statically analyzing a validation toolkit environment. The method may also include, identifying a plurality of computational threads that do not share data structures with each other based on analysis of the validation toolkit environment. The method may additionally include calculating computational requirements of the computational threads. The method may further include distributing the threads among a plurality of resources such that the aggregate computational requirements of the computational threads are approximately evenly balanced among the plurality of resources.

Systems and methods for distributing validation computations

In one embodiment, a method includes accessing an event-driven application input by a user, the event-driven application comprising source code, one or more use cases input by the user for the event-driven application, and one or more functional requirements input by the user for the event-driven application; parsing the use cases and the functional requirements according to the predefined syntax to construct one or more validation modules for validating the event-driven application without any modification to the source code of the event-driven application for validation purposes; formally validating the event-driven application using the validation modules without relying on assertions inserted into the source code of the event-driven application for validation purposes; and if the formal validation finds one or more defects in the event-driven application, generating output for communication to the user identifying the defects.

Growing community of inventors

Sunnyvale, CA, United States of America

Sreeranga P Rajan