| Patent application number | Description | Published |
|---|
| 20090094004 | METHODS AND SYSTEMS FOR EFFICIENT ANALYSIS OF HYBRID SYSTEMS USING TEMPLATE POLYHEDRA - 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. | 04-09-2009 |
| 20090192963 | SYSTEM AND METHOD FOR DYNAMICALLY INFERRING DATA PRECONDITIONS OVER PREDICATES BY TREE LEARNING - 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. | 07-30-2009 |
| 20090193401 | PATH-SENSITIVE ANALYSIS THROUGH INFEASIBLE-PATH DETECTION AND SYNTACTIC LANGUAGE REFINEMENT - 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. | 07-30-2009 |
| 20100005454 | PROGRAM VERIFICATION THROUGH SYMBOLIC ENUMERATION OF CONTROL PATH PROGRAMS - 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. | 01-07-2010 |
| 20100058475 | FEEDBACK-GUIDED FUZZ TESTING FOR LEARNING INPUTS OF COMA - Embodiments of the present invention combine static analysis, source code instrumentation and feedback-guided fuzz testing to automatically detect resource exhaustion denial of service attacks in software and generate inputs of coma for vulnerable code segments. The static analysis of the code highlights portions that are potentially vulnerable, such as loops and recursions whose exit conditions are dependent on user input. The code segments are dynamically instrumented to provide a feedback value at the end of each execution. Evolutionary techniques are then employed to search among the possible inputs to find inputs that maximize the feedback score. | 03-04-2010 |
| 20100094611 | SYSTEM AND METHOD FOR FEEDBACK-GUIDED TEST GENERATION FOR CYBER-PHYSICAL SYSTEMS USING MONTE-CARLO - A system and method for generating test vectors includes generating traces of a system model or program stored in memory using a simulation engine. Simulated inputs are globally optimized using a fitness objective computed using a computer processing device. The simulation inputs are adjusted in accordance with feedback from the traces and fitness objective values by computing a distance between the fitness objective value and a reachability objective. Test input vectors are output based upon optimized fitness objective values associated with the simulated inputs to test the system model or program stored in memory. | 04-15-2010 |
| 20100281086 | EFFICIENT DECISION METHOD FOR REAL NON-LINEAR ARITHMETIC CONSTRAINTS - A system and method for solving a decision problem having Boolean combinations of linear and non-linear operations includes translating the non-linear real operations using a COordinate Rotation DIgital Computer (CORDIC) method programmed on a computer device into linear operations maintaining a given accuracy. Linear and translated linear operations are combined into a formula. Satisfiablity of the formula is solved using a decision procedure for Boolean combinations of linear operations over integers and reals. | 11-04-2010 |
| 20100293530 | SYSTEMS AND METHODS FOR MODEL CHECKING THE PRECISION OF PROGRAMS EMPLOYING FLOATING-POINT OPERATIONS - Methods and systems for verifying the precision of a program that utilizes floating point operations are disclosed. Interval and affine arithmetic can be employed to build a model of the program including floating point operations and variables that are expressed as reals and integers, thereby permitting accurate determination of precision loss using a model checker. Abstract interpretation can be also employed to simplify the model. In addition, counterexample-guided abstraction refinement can be used to refine the values of parametric error constants introduced in the model. | 11-18-2010 |
| 20100299651 | ROBUST TESTING FOR DISCRETE-TIME AND CONTINUOUS-TIME SYSTEM MODELS - A system and method for testing robustness of a simulation model of a cyber-physical system includes computing a set of symbolic simulation traces for a simulation model for a continuous time system stored in memory, based on a discrete time simulation of given test inputs stored in memory. Simulation errors are accounted for due to at least one of numerical instabilities and numeric computations. The set of symbolic simulation traces are validated with respect to validation properties in the simulation model. Portions of the simulation model description are identified that are sources of the simulation errors. | 11-25-2010 |
