Patent application number | Description | Published |
20120110550 | NODE COMPUTATION INITIALIZATION TECHNIQUE FOR EFFICIENT PARALLELIZATION OF SOFTWARE ANALYSIS IN A DISTRIBUTED COMPUTING ENVIRONMENT - A method for verifying software includes determining an initialization path condition of a received software verification job, determining a termination path condition of a computing node, and initializing the execution of the received software verification job on the computing node based on the initialization path condition and the termination path condition. The initialization path condition includes a sequence of program predicates for reaching a starting state of software to be verified. The received software verification job includes an indication of a portion of the software to be verified. The termination path condition includes an indication of the last state reached during the execution of a previous software verification job on the computing node. The computing node is assigned to execute the received software verification job. | 05-03-2012 |
20120110580 | DYNAMIC AND INTELLIGENT PARTIAL COMPUTATION MANAGEMENT FOR EFFICIENT PARALLELIZATION OF SOFTWARE ANALYSIS IN A DISTRIBUTED COMPUTING ENVIRONMENT - A method for verifying software includes determining the result of a bounding function, and using the result of the bounding function to apply one or more policies to the execution of the received job. The bounding function evaluates the execution of a received job, the received job indicating a portion of software to be verified. The result of the bounding function is based upon the present execution of the received job, one or more historical parameters, and an evaluation of the number of idle nodes available to process other jobs. | 05-03-2012 |
20120110589 | TECHNIQUE FOR EFFICIENT PARALLELIZATION OF SOFTWARE ANALYSIS IN A DISTRIBUTED COMPUTING ENVIRONMENT THROUGH INTELLIGENT DYNAMIC LOAD BALANCING - A method for verifying software includes monitoring a resource queue and a job queue, determining whether the resource queue and the job queue contain entries, and if both the resource queue and the job queue contain entries, then applying a scheduling policy to select a job, selecting a worker node as a best match for the characteristics of the job among the resource queue entries, assigning the job to the worker node, assigning parameters to the worker node for a job creation policy for creating new jobs in the job queue while executing the job, and assigning parameters to the worker node for a termination policy for halting execution of the job. The resource queue indicates worker nodes available to verify a portion of code. The job queue indicates one or more jobs to be executed by a worker node. A job includes a portion of code to be verified. | 05-03-2012 |
20120110590 | EFFICIENT PARTIAL COMPUTATION FOR THE PARALLELIZATION OF SOFTWARE ANALYSIS IN A DISTRIBUTED COMPUTING ENVIRONMENT - An electronic device includes a memory, a processor coupled to the memory, and one or more policies stored in the memory. The policies include a resource availability policy determining whether the processor should continue evaluating the software, and a job availability policy determining whether new jobs will be created for unexplored branches. The processor is configured to receive a job to be executed, evaluate the software, select a branch to explore and store an initialization sequence of one or more unexplored branches if a branch in the software is encountered, evaluate the job availability policy, decide whether to create a job for each of the unexplored branches based on the job availability policy, evaluate the resource availability policy, and decide whether to continue evaluating the software at the branch selected to explore based on the resource availability policy. The job indicates of a portion of software to be evaluated. | 05-03-2012 |
20120110591 | SCHEDULING POLICY FOR EFFICIENT PARALLELIZATION OF SOFTWARE ANALYSIS IN A DISTRIBUTED COMPUTING ENVIRONMENT - A method for verifying software includes accessing a job queue, accessing a resource queue, and assigning a job from the job queue to a resource from the resource queue if an addition is made to the a job queue or to a resource queue. The job queue includes an indication of one or more jobs to be executed by a worker node, each job indicating a portion of a code to be verified. The resource queue includes an indication of a one or more worker nodes available to verify a portion of software. The resource is selected by determining the best match for the characteristics of the selected job among the resources in the resource queue. | 05-03-2012 |
20120192150 | Software Architecture 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. | 07-26-2012 |
20120192162 | Optimizing Handlers for Application-Specific Operations for Validating C++ Programs Using Symbolic Execution - 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. | 07-26-2012 |
20120192169 | Optimizing Libraries for Validating C++ Programs Using Symbolic Execution - 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. | 07-26-2012 |
20120204154 | Symbolic Execution and Test Generation for GPU Programs - 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. | 08-09-2012 |
20120265357 | Measure Energy Consumption and Determine Energy-Consumption Patterns for Electricity-Consuming Devices - In one embodiment, one or more electronic devices access energy-consumption data at each of a plurality of electricity-consuming devices, the energy-consumption data at each of the electricity-consuming devices indicating for each of a plurality of past pre-determined time periods an aggregate energy usage by the electricity-consuming device over the past pre-determined time period, an energy-measurement unit at the electricity-consuming device having measured and recorded the aggregate energy usage by the electricity-consuming device for each of the past pre-determined time periods for later access, each of the energy-measurement units having a substantially unique identifier (ID), each of the electricity-consuming devices having its own one of the energy-measurement units; and based on the energy-consumption data, determine one or more energy-consumption patterns across the electricity-consuming devices over at least the past pre-determined time periods. | 10-18-2012 |
20120311545 | Lossless Path Reduction for Efficient Symbolic Execution and Automatic Test Generation - 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. | 12-06-2012 |
20130318503 | SYMBOLIC EXECUTION AND AUTOMATIC TEST CASE GENERATION FOR JAVASCRIPT PROGRAMS - 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. | 11-28-2013 |
20130326485 | RULE-BASED METHOD FOR PROVING UNSATISFIABLE CONDITIONS IN A MIXED NUMERIC AND STRING SOLVER - 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. | 12-05-2013 |
20140019939 | Iterative Generation of Symbolic Test Drivers for Object-Oriented Languages - A method includes, by one or more computing devices, determining instructions for a computing device to be evaluated, creating a first symbolic test driver including one or more of the instructions to be evaluated and a designation of a symbolic variable corresponding to a portion of the instructions, symbolically executing the instructions with respect to the symbolic variable, determining a test case from the results of the symbolic execution including one or more commands to execute the instructions with a given value for the symbolic variable, determining one or more calls to an object-oriented-programming component in the commands, creating a new symbolic test driver including the calls based on the determined calls, and subsequently symbolically executing the new symbolic test driver. | 01-16-2014 |
20140047217 | SATISFIABILITY CHECKING - 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. | 02-13-2014 |
20140053134 | SOFTWARE REGRESSION TESTING USING SYMBOLIC EXECUTION - A method of testing software may include accessing first software that includes multiple execution paths and concretely executing the first software using a test case associated with second software to traverse at least a first execution path of the execution paths. The method may also include capturing concrete execution results produced from concretely executing the first software to record the first execution path and symbolically executing the first software using a symbolic input based on the recorded first execution path. | 02-20-2014 |
20140082594 | ABSTRACT SYMBOLIC EXECUTION FOR SCALING SYMBOLIC EXECUTION GENERATION AND AUTOMATIC TEST GENERATION - 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. | 03-20-2014 |
20140143604 | MIXED NUMERIC AND STRING CONSTRAINT ANALYSIS - A method of determining whether a set of constraints is satisfiable may include identifying a set of constraints associated with a software module. The method may also include modeling a string associated with a string constraint of the set of constraints as a parameterized array. Further, the method may include determining the satisfiability of the set of constraints based on a representation of the string constraint as a quantified expression. The satisfiability of the set of constraints may also be based on elimination of a quantifier associated with the quantified expression such that the string constraint is represented as a numeric constraint. The representation of the string constraint as a quantified expression may be based on the parameterized array that is associated with the string. | 05-22-2014 |
20140143762 | SYMBOLIC EXECUTION OF DYNAMIC PROGRAMMING LANGUAGES - A method of symbolically executing a dynamic program may include receiving a portion of a dynamic program that includes multiple objects. The method may also include symbolically executing the dynamic program including constraint solving by managing runtime states of the symbolic execution within a native symbolic executor. Managing the runtime states of the symbolic execution may include constructing an object map of two or more of the objects that are interdependent and distinguishing code portions of one of the two or more objects in the object map from data portions of the one of the two or more objects. Managing the runtime states of the symbolic execution may also include performing one or more of state copying, state backtracking, state sharing, and state spawning based on characteristics of the dynamic program using the object map and the distinguished code portions and data portions. | 05-22-2014 |