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 |
20100011057 | PARALLELIZING BOUNDED MODEL CHECKING USING TUNNELS OVER A DISTRIBUTED FRAMEWORK - A system and method for bounded model checking of computer programs includes decomposing a program having at least one reachable property node for bounded model checking (BMC) into sub-problems by employing a tunneling and slicing-based (TSR) BMC reduction method. The sub-problems of the TSR method are partitioned in a distributed environment, where the distributed environment includes at least one master processing unit and at least one client unit. The sub-problems are solved by each client independently of other clients to reduce communication overhead and provide scalability. | 01-14-2010 |
20100251222 | COMPLETENESS DETERMINATION IN SMT-BASED BMC FOR SOFTWARE PROGRAMS - A computer implemented method for obtaining a completeness threshold (CT) in Bounded Model Checking systems for software programs. | 09-30-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 |
20110246970 | INTERVAL ANALYSIS OF CONCURRENT TRACE PROGRAMS USING TRANSACTION SEQUENCE GRAPHS - A method for the verification of multi-threaded computer programs through the use of concurrent trace programs (CTPs) and transaction sequence graphs (TSGs). | 10-06-2011 |
20130205303 | Efficient Checking of Pairwise Reachability in Multi-Threaded Programs - Disclosed is a simple but yet effective strategy to check pairwise reachability in an online analysis under a general locking scheme where locks may be acquired in recursive, non-nested, or nested manner. Under data abstraction, such an approach guarantees true positives and negatives for two-threaded system. For more than two threaded, it guarantees either true positive or true negative (but not both). It uses time stamped lock/unlock events to identify and avoid redundant and inconsistent sequence. Importantly, the approach is incremental and reduce amortized cost of checking multiple pairwise reachability problems. The worst case complexity is quadratic in the length of the history; in practice, however, the running cost is linear in the length of the history. Such an approach improves the accuracy of the race prediction for general locking style that includes recursive, nesting/non-nesting, and thereby improving the overall runtime verification | 08-08-2013 |
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 |
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 |