公开(公告)号：US20100281469A1

公开(公告)日：2010-11-04

申请号：US12726764

申请日：2010-03-18

申请人： Chao Wang ,  Malay Ganai ,  Aarti Gupta

发明人： Chao Wang ,  Malay Ganai ,  Aarti Gupta

IPC分类号： G06F9/44

CPC分类号： G06F11/3612 ,  G06F8/45 ,  G06F11/3636

摘要： 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.

摘要翻译： 显示了一种用于在并发程序中发现断言违规和原子性违规的符号预测分析方法，该方法为给定测试下的程序导出并发跟踪程序（CTP）。 然后，基于CTP的并发静态单赋值（CSSA）表示形式生成逻辑公式，包括至少一个断言属性或原子性冲突。 然后确定公式的可满足性，使得确定的结果表示断言/原子性违规。

公开(公告)号：US20090282288A1

公开(公告)日：2009-11-12

申请号：US12397696

申请日：2009-03-04

申请人： Chao Wang ,  Aarti Gupta

发明人： Chao Wang ,  Aarti Gupta

IPC分类号： G06F11/07

CPC分类号： G06F11/3612

摘要： 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.

摘要翻译： 用于并行系统的用于动态数据竞争检测的系统和方法包括使用用于并发系统的不同组件的处理器来计算锁定信息。 执行系统的受控执行，其中受控执行探讨并发组件的不同交织。 在受控执行期间使用锁定信息来检查与执行中的状态相关联的搜索子空间是否没有数据竞争。 动态修剪无竞争的搜索子空间，以减少资源的使用。

公开(公告)号：US20090204968A1

公开(公告)日：2009-08-13

申请号：US12367140

申请日：2009-02-06

申请人： Vineet Kahlon ,  Chao Wang ,  Aarti Gupta

发明人： Vineet Kahlon ,  Chao Wang ,  Aarti Gupta

IPC分类号： G06F9/44

CPC分类号： G06F11/3604 ,  G06F11/30

摘要： 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.

摘要翻译： 一种用于分析并发程序的系统和方法，保证要探索的线程间隔数量的最优化。 通过全局约束其线程的本地操作的离开来确保优化，从而仅探索准单调序列的线程操作。 为了效率，使用SAT / SMT求解器来探索给定并发程序的准单调计算。 通过SAT / SMT求解器在并发程序的探索期间动态添加约束，以确保模型检查的准单调性。

公开(公告)号：US20090007038A1

公开(公告)日：2009-01-01

申请号：US11950730

申请日：2007-12-05

申请人： Chao Wang ,  Aarti Gupta ,  Hyondeuk Kim

发明人： Chao Wang ,  Aarti Gupta ,  Hyondeuk Kim

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： 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.

摘要翻译： 公开了用于通过将设计变换成功能等同的控制和数据流图（CDFG）来执行反例引导的抽象改进的系统和方法; 执行设计的混合抽象; 产生混合抽象模型; 并检查混合抽象模型。

公开(公告)号：US08359578B2

公开(公告)日：2013-01-22

申请号：US12571476

申请日：2009-10-01

申请人： Chao Wang ,  Aarti Gupta ,  Swarat Chaudhuri ,  Yu Yang

发明人： Chao Wang ,  Aarti Gupta ,  Swarat Chaudhuri ,  Yu Yang

IPC分类号： G06F9/44

CPC分类号： G06F11/3612 ,  G06F11/3624 ,  G06F11/3636

摘要： 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.

摘要翻译： 一种用于验证并发软件程序的计算机实现方法，其中并发软件程序被划分为称为并发跟踪程序（CTP）的子集，并且使用基于可满足性（SAT）符号分析来评估每个CTP。 通过将SAT分析应用于独立的CTP，符号分析有利地更具可扩展性和高效性。

公开(公告)号：US08200474B2

公开(公告)日：2012-06-12

申请号：US12397696

申请日：2009-03-04

申请人： Chao Wang ,  Aarti Gupta

发明人： Chao Wang ,  Aarti Gupta

IPC分类号： G06F9/45

CPC分类号： G06F11/3612

摘要： 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.

摘要翻译： 用于并行系统的用于动态数据竞争检测的系统和方法包括使用用于并发系统的不同组件的处理器来计算锁定信息。 执行系统的受控执行，其中受控执行探讨并发组件的不同交织。 在受控执行期间使用锁定信息来检查与执行中的状态相关联的搜索子空间是否没有数据竞争。 动态修剪无竞争的搜索子空间，以减少资源的使用。

公开(公告)号：US07926039B2

公开(公告)日：2011-04-12

申请号：US11692421

申请日：2007-03-28

申请人： Chao Wang ,  Zijiang Yang ,  Aarti Gupta

发明人： Chao Wang ,  Zijiang Yang ,  Aarti Gupta

IPC分类号： G06F9/44 ,  G06F9/45

CPC分类号： G06F9/44589

摘要： An improved method for automatically improving the precision of an extrapolation operator used, for example, in software program verification in connection with the static analysis and model checking of the software programs which rely on fix-point computation. In particular, a new extrapolation-with-care-set operator, together with a method for gradually increasing the precision of this operation by tightening the care set.

摘要翻译： 一种改进的方法，用于自动提高外推算子的精度，例如，在依赖于固定点计算的软件程序的静态分析和模型检查的软件程序验证中。 特别地，一种新的外推护理操作器，以及通过收紧护理套件逐渐增加该操作的精度的方法。

公开(公告)号：US20120089873A1

公开(公告)日：2012-04-12

申请号：US13081684

申请日：2011-04-07

申请人： Chao Wang ,  Aarti Gupta

发明人： Chao Wang ,  Aarti Gupta

IPC分类号： G06F11/36

CPC分类号： G06F11/3688 ,  G06F11/3624

摘要： 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.

摘要翻译： 系统和方法通过在共享对象访问上动态学习HaPSet排序约束来提供覆盖引导的系统测试框架; 并应用学习的HaPSet排序约束来选择高风险的交织以供将来测试执行。

公开(公告)号：US07693690B2

公开(公告)日：2010-04-06

申请号：US11367665

申请日：2006-03-03

申请人： Chao Wang ,  Aarti Gupta ,  Zijiang Yang ,  Franjo Ivancic

发明人： Chao Wang ,  Aarti Gupta ,  Zijiang Yang ,  Franjo Ivancic

IPC分类号： G06F17/50 ,  G06F13/00

CPC分类号： G06F11/3608 ,  G06F17/504

摘要： A symbolic disjunctive image computation method for software models which exploits a number of characteristics unique to software models. More particularly, and according to our inventive method, the entire software model is decomposed into a disjunctive set of submodules and a separate set of transition relations are constructed. An image/reachability analysis is performed wherein an original image computation is divided into a set of image computation steps that may be performed on individual submodules, independently from any others. Advantageously, our inventive method exploits variable locality during the decomposition of the original model into the submodules. By formulating this decomposition as a multi-way hypergraph partition problem, we advantageously produce a small set of submodules while simultaneously minimizing the number of live variable in each individual submodule. Our inventive method produces a set of disjunctive transition relations directly from the software model, without producing a conjunctive transition relation—as is necessary in the prior art. In addition, our inventive method exploits the exclusive use of live variables in addition to novel search strategies which provide still further benefit to our method.

摘要翻译： 用于软件模型的符号分离图像计算方法，其利用软件模型独特的许多特征。 更具体地，根据本发明的方法，整个软件模型被分解成一个分离的子模块集合，并构建了一组单独的过渡关系。 执行图像/可达性分析，其中原始图像计算被划分为可以独立于任何其他方式对各个子模块执行的一组图像计算步骤。 有利地，本发明的方法在原始模型分解成子模块期间利用可变局部性。 通过将此分解形式作为多路超图分区问题，我们有利地产生一小组子模块，同时最小化每个子模块中的实时变量数量。 我们的创造性方法直接从软件模型产生一组分离过渡关系，而不产生结合过渡关系 - 这在现有技术中是必需的。 此外，除了新颖的搜索策略之外，我们的创造性方法还利用了实时变量的独家使用，这为我们的方法提供了更多的益处。

公开(公告)号：US08381226B2

公开(公告)日：2013-02-19

申请号：US12367140

申请日：2009-02-06

申请人： Vineet Kahlon ,  Chao Wang ,  Aarti Gupta

发明人： Vineet Kahlon ,  Chao Wang ,  Aarti Gupta

IPC分类号： G06F11/36

CPC分类号： G06F11/3604 ,  G06F11/30

摘要： 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.

摘要翻译： 一种用于分析并发程序的系统和方法，保证要探索的线程间隔数量的最优化。 通过全局约束其线程的本地操作的离开来确保优化，从而仅探索准单调序列的线程操作。 为了效率，使用SAT / SMT求解器来探索给定并发程序的准单调计算。 通过SAT / SMT求解器在并发程序的探索期间动态添加约束，以确保模型检查的准单调性。