Patent application number | Description | Published |
20080281563 | MODELING AND VERIFICATION OF CONCURRENT SYSTEMS USING SMT-BASED BMC - A computer implemented method for modeling and verifying concurrent systems which uses Satisfiability-Modulo Theory (SMT)-based Bounded Model Checking (BMC) to detect violations of safety properties such as data races. A particularly distinguishing aspect of our inventive method is that we do not introduce wait-cycles in our symbolic models for the individual threads, which are typically required for considering an interleaved execution of the threads. These wait-cycles are detrimental to the performance of BMC. Instead, we first create independent models for the different threads, and add inter-model constraints lazily, incrementally, and on-the-fly during BMC unrolling to capture the sequential consistency and synchronization semantics. We show that our constraints provide a sound and complete modeling with respect to the considered semantics. One benefit of our lazy modeling method is the reduction in the size of the BMC problem instances, thereby, improving the verification performance in both runtime and memory. | 11-13-2008 |
20080282221 | ACCELERATING MODEL CHECKING VIA SYNCHRONY - A system and method for program verification by model checking in concurrent programs includes modeling each of a plurality of program threads as a circuit model, and generating a full circuit for an entire program by combining the circuit models including constraints which enforce synchronous execution of the program threads. The program is verified using the synchronous execution to reduce an amount of memory needed to verify the program and a number of steps taken to uncover an error. | 11-13-2008 |
20090007038 | HYBRID COUNTEREXAMPLE GUIDED ABSTRACTION REFINEMENT - Systems and methods are disclosed for performing counterexample guided abstraction refinement by transforming a design into a functionally equivalent Control and Data Flow Graph (CDFG); performing a hybrid abstraction of the design; generating a hybrid abstract model; and checking the hybrid abstract model. | 01-01-2009 |
20090064110 | MINING LIBRARY SPECIFICATIONS USING INDUCTIVE LEARNING - A system and method for mining program specifications includes generating unit tests to exercise functions of a library through an application program interface (API), based upon an (API) signature. A response to the unit tests is determined to generate a transaction in accordance with a target behavior. The transaction is converted into a relational form, and specifications of the library are learned using an inductive logic programming tool from the relational form of the transaction. | 03-05-2009 |
20090089783 | PARTIAL ORDER REDUCTION USING GUARDED INDEPENDENCE RELATIONS - A system and method for conducting symbolic partial order reduction for concurrent systems includes determining a guarded independence relation which includes transitions from different threads that are independent for a set of states, when a condition or predicate holds. Partial order reduction is performed using the guarded independence relation to permit automatic pruning of redundant thread interleavings when the guarded independence condition holds. | 04-02-2009 |
20090125887 | SYSTEM AND METHOD FOR GENERATING ERROR TRACES FOR CONCURRENCY BUGS - A system and method for program verification includes generating a product transaction graph for a concurrent program, which captures warnings for potential errors. The warnings are filtered to remove bogus warnings, by using constraints from synchronization primitives and invariants that are derived by performing one or more dataflow analysis methods for concurrent programs. The dataflow analysis methods are applied in order of overhead expense. Concrete execution traces are generated for remaining warnings using model checking. | 05-14-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 |
20090204968 | SYSTEM AND METHOD FOR MONOTONIC PARTIAL ORDER REDUCTION - A system and method for analyzing concurrent programs that guarantees optimality in the number of thread inter-leavings to be explored. Optimality is ensured by globally constraining the inter-leavings of the local operations of its threads so that only quasi-monotonic sequences of threads operations are explored. For efficiency, a SAT/SMT solver is used to explore the quasi-monotonic computations of the given concurrent program. Constraints are added dynamically during exploration of the concurrent program via a SAT/SMT solver to ensure quasi-montonicity for model checking. | 08-13-2009 |
20090222249 | MODULAR VERIFICATION OF WEB SERVICES USING EFFICIENT SYMBOLIC ENCODING AND SUMMARIZATION - A system and method for verifying a composition of interacting services in a distributed system includes generating a concurrent process graph (CPG) for processes in a system and symbolically encoding the CPG of each process to perform a reachability analysis. Symbolic summaries are generated for concurrently running processes based on the reachability analysis. Modular verification is conducted by utilizing the symbolic summaries of the processes to verify a system of interrelated processes. | 09-03-2009 |
20090282288 | DYNAMIC MODEL CHECKING WITH PROPERTY DRIVEN PRUNING TO DETECT RACE CONDITIONS - A system and method for dynamic data race detection for concurrent systems includes computing lockset information using a processor for different components of a concurrent system. A controlled execution of the system is performed where the controlled execution explores different interleavings of the concurrent components. The lockset information is used during the controlled execution to check whether a search subspace associated with a state in the execution is free of data races. A race-free search subspace is dynamically pruned to reduce resource usage. | 11-12-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 |
20100088681 | SYMBOLIC REDUCTION OF DYNAMIC EXECUTIONS OF CONCURRENT PROGRAMS - A computer implemented method for the verification of concurrent software programs wherein the concurrent software program is partitioned into subsets named concurrent trace programs (CTPs) and each of the CTPs is evaluated using a satisfiability-based (SAT) symbolic analysis. By applying the SAT analysis to individual CTPs in isolation the symbolic analysis is advantageously more scalable and efficient. | 04-08-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 |
20100205592 | CONTROL STRUCTURE REFINEMENT OF LOOPS USING STATIC ANALYSIS - 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. | 08-12-2010 |
20100281469 | SYMBOLIC PREDICTIVE ANALYSIS FOR CONCURRENT PROGRAMS - A symbolic predictive analysis method for finding assertion violations and atomicity violations in concurrent programs is shown that derives a concurrent trace program (CTP) for a program under a given test. A logic formula is then generated based on a concurrent static single assignment (CSSA) representation of the CTP, including at least one assertion property or atomicity violation. The satisfiability of the formula is then determined, such that the outcome of the determination indicates an assertion/atomicity violation. | 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 |
20110173148 | INTEGRATING INTERVAL CONSTRAINT PROPAGATION WITH NONLINEAR REAL ARITHMETIC - A system and method for deciding the satisfiability of a non-linear real decision problem is disclosed. Linear and non-linear constraints associated with the problem are separated. The feasibility of the linear constraints is determined using a linear solver. The feasibility of the non-linear constraints is determined using a non-linear solver which employs interval constraint propagation. The interval solutions obtained from the non-linear solver are validated using the linear solver. If the solutions cannot be validated, linear constraints are learned to refine a search space associated with the problem. The learned constraints and the non-linear constraints are iteratively solved using the non-linear solver until either a feasible solution is obtained or no solution is possible. | 07-14-2011 |
20120084761 | Interprocedural Exception Method - 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. | 04-05-2012 |
20120089873 | SYSTEMS AND METHODS FOR AUTOMATED SYSTEMATIC CONCURRENCY TESTING - Systems and method provide a coverage-guided systematic testing framework by dynamically learning HaPSet ordering constraints over shared object accesses; and applying the learned HaPSet ordering constraints to select high-risk interleavings for future test execution. | 04-12-2012 |
20120117547 | EMBEDDING CLASS HIERARCHY INTO OBJECT MODELS FOR MULTIPLE CLASS INHERITANCE - 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. | 05-10-2012 |
20120151449 | Scope Bounding with Automated Specification Inference for Scalable Software Model Checking - A scalable, computer implemented method for finding subtle flaws in software programs. The method advantageously employs 1) scope bounding which limits the size of a generated model by excluding deeply-nested function calls, where the scope bounding vector is chosen non-monotonically, and 2) automatic specification inference which generates constraints for functions through the effect of a light-weight and scalable global analysis. Advantageously, scalable software model checking is achieved while at the same time finding more bugs. | 06-14-2012 |
20120179935 | DYNAMIC TEST GENERATION FOR CONCURRENT PROGRAMS - A computer implemented method for dynamic test generation for concurrent programs, which uses a combination of concrete and symbolic execution of the program to systematically cover all the intra-thread program branches and inter-thread interleavings of shared accesses. In addition, a coverage summary based pruning technique, which is a general framework for soundly removing both redundant paths and redundant interleavings and is capable of speeding up dynamic testing exponentially. This pruning framework also allows flexible trade-offs between pruning power and computational overhead to be exploited using various approximations. | 07-12-2012 |
20120233584 | Analysis of Interactions of C and C++ Strings - 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. | 09-13-2012 |
20130091495 | FEEDBACK-DIRECTED RANDOM CLASS UNIT TEST GENERATION USING SYMBOLIC EXECUTION - Methods and systems for generating software analysis test inputs include generating a path query to cover a target branch of a program by executing a symbolic test driver concretely and partially symbolically, where at least one symbolic expression is partially concretized with concrete values; determining whether it is feasible to execute the target branch based on whether the generated path query is satisfiable or unsatisfiable using a constraint solver; if the target branch is feasible, generating a new test driver by replacing symbolic values in the symbolic test driver with generated solution values; and if the target branch is not feasible, analyzing an unsatisfiable core to determine whether unsatisfiability is due to a concretization performed during generation of the path query. | 04-11-2013 |
20130227537 | CONTROL STRUCTURE REFINEMENT OF LOOPS USING STATIC ANALYSIS - 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. | 08-29-2013 |
20130332906 | CONCURRENT TEST GENERATION USING CONCOLIC MULTI-TRACE ANALYSIS - A method to test a concurrent program by performing a concolic multi-trace analysis (CMTA) to analyze the concurrent program by taking two or more test runs over many threads and generating a satisfiability modulo theory (SMT) formula to select alternate inputs, alternate schedules and parts of threads from one or more test runs; using an SMT solver on the SMT formula for generating a new concurrent test comprising input values, thread schedules and parts of thread selections; and executing the new concurrent test. | 12-12-2013 |
20140019946 | LAYERED DECOMPOSITION FOR SCALABLE STATIC DATA RACE DETECTION OF CONCURRENT PROGRAMS - Disclosed is a method of performing static data race detection in concurrent programs wherein a control flow graph (CFG) is decomposed into layers of bounded call-depth which are then used to perform a resulting analysis. Next, a set of pointers of interest are segmented into classes such that each pointer may only be aliased to pointers within its own class, these classes related to computation of shared variables, locksets, waitsets, and notifysets. A flow sensitive context sensitive points-to-analysis for program statements that impact aliases of members within the given class is performed—advantageously reducing the overall size of the problem at hand. Notably, the analysis for individual threads is performed independently of one another, on multiple layers of the CFG, and subsequently merging the results from the individual layers. | 01-16-2014 |
20140108867 | Dynamic Taint Analysis of Multi-Threaded Programs - Disclosed is a dynamic taint analysis framework for multithreaded programs (DTAM) that identifies a subset of program inputs and shared memory accesses that are relevant for issues related to concurrency. Computer implemented methods according to the framework generally involve the computer implemented steps of: applying independently a dynamic taint analysis to each of the multiple threads comprising a multi-threaded computer program; aggregating each independent result from the analysis for each of the multiple threads by consolidating effect of taint analysis in one or more possible re-orderings of observed shared memory accesses among threads; and outputting an indicia of the aggregated result as a set of relevant program inputs or a set of relevant shared memory accesses. | 04-17-2014 |
20140289712 | Effective Lifetime Dependency Analysis and Typestate Analysis - Disclosed are typestate and lifetime dependency analysis methods for identifying bugs in C++ programs. Disclosed are an abstract representation (ARC++) that models C++ objects and which makes object creation/destruction, usage, lifetime and pointer operations explicit in the abstract model thereby providing a basis for static analysis on the C++ program. Also disclosed is a lifetime dependency analysis that tracks implied dependency relationships between lifetimes of objects, to capture an effective high-level abstraction for issues involving temporary objects and internal buffers, and subsequently used in the static analysis that supports typestate checking for the C++ program. Finally disclosed a framework that automatically genarates ARC++ representations from C++ programs and performs typestate checking to detect bugs that are specified as typestate automata over ARC++ representations. | 09-25-2014 |
20140337674 | Network Testing - A network testing method implemented in a software-defined network (SDN) is disclosed. The network testing method comprising providing a test scenario including one or more network events, injecting said one or more network events to the SDN using an SDN controller, and gathering network traffic statistics. A network testing apparatus used in a software-defined network (SDN) also is disclosed. The network testing apparatus comprising a testing system to provide a test scenario including one or more network events, to inject said one or more network events to the SDN using an SDN controller, and to gather network traffic statistics. Other methods, apparatuses, and systems also are disclosed. | 11-13-2014 |
20150081243 | Setsudo: Pertubation-based Testing Framework for Scalable Distributed Systems - Disclosed are a testing framework—SETSUD Ō—that uses perturbation-based exploration for robustness testing of modern scalable distributed systems. In sharp contrast to existing testing techniques and tools that are limited in that they are typically based on black-box approaches or they focus mostly on failure recovery testing, SETSUD Ō is a flexible framework to exercise various perturbations to create stressful scenarios. SETSUD Ō is built on an underlying instrumentation infrastructure that provides abstractions of internal states of the system as labeled entities. Both novice and advanced testers can use these labeled entities to specify scenarios of interest at the high level, in the form of a declarative style test policy. SETSUD Ō automatically generates perturbation sequences and applies them to system-level implementations, without burdening the tester with low-level details. | 03-19-2015 |