公开(公告)号：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）来执行反例引导的抽象改进的系统和方法; 执行设计的混合抽象; 产生混合抽象模型; 并检查混合抽象模型。

公开(公告)号：US08522226B2

公开(公告)日：2013-08-27

申请号：US12701962

申请日：2010-02-08

申请人： Sriram Sankaranarayanan ,  Aarti Gupta ,  Gogul Balakrishnan

发明人： Sriram Sankaranarayanan ,  Aarti Gupta ,  Gogul Balakrishnan

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

CPC分类号： G06F8/443 ,  G06F8/433

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

公开(公告)号：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.

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

公开(公告)号：US20070011671A1

公开(公告)日：2007-01-11

申请号：US11174791

申请日：2005-07-05

申请人： Vineet Kahlon ,  Aarti Gupta

发明人： Vineet Kahlon ,  Aarti Gupta

IPC分类号： G06F9/44

CPC分类号： G06F9/52 ,  G06F11/3608

摘要： A method for the static analysis of concurrent multi-threaded software which bypasses the state explosion situation that plagues the prior art, thereby making our method scalable while—at the same time—producing no loss in precision. Our inventive method maintains patterns of lock acquisition and lock release by individual threads by constructing augmented versions of the threads. Once the augmented versions have been constructed, our inventive method verifies the concurrent program using existing tools for the verification of sequential programs—thereby greatly reducing implementation overhead. Finally, our inventive augmentation and method is carried out in an automatic manner—without requiring user intervention.

摘要翻译： 一种用于并发多线程软件的静态分析方法，绕过了现有技术的状态爆炸情况，从而使我们的方法可扩展，同时产生精度上的损失。 本发明的方法通过构造线程的扩展版本来维护单独线程的锁获取和锁定释放模式。 一旦增强版本被构建，我们的创造性方法使用现有工具来验证并发程序来验证顺序程序，从而大大降低了实现开销。 最后，我们的创造性增加和方法是以自动的方式进行的 - 不需要用户干预。

公开(公告)号：US6026222A

公开(公告)日：2000-02-15

申请号：US997551

申请日：1997-12-23

申请人： Aarti Gupta ,  Pranav N Ashar

发明人： Aarti Gupta ,  Pranav N Ashar

IPC分类号： H01L21/822 ,  G06F17/50 ,  H01L21/66 ,  H01L27/04

CPC分类号： G06F17/504

摘要： A computer system, computer program product, and method for solving a combinational logic verification problem with respect to two combinational circuits includes Boolean SAT checking integrated with binary decision diagrams (BDD) use. A fanout partition of a miter circuit formed from the two combinational circuits is reduced to BDD form, while the fanin partition is represented by SAT clauses. As SAT solutions are evaluated, variables in the cutset between the fanout and fanin partitions are assigned values. In a preferred embodiment, each assignment to a cutset variable is checked against an onset of the BDD prior to continuing with SAT solution seeking.

摘要翻译： 一种计算机系统，计算机程序产品和用于解决两个组合电路组合逻辑验证问题的方法，包括与二进制决策图（BDD）使用集成的布尔SAT检查。 由两个组合电路形成的斜角电路的扇出分区减少为BDD形式，而扇形分区由SAT子句表示。 在评估SAT解决方案时，扇出分区和扇区分区之间的变量将分配值。 在优选实施例中，在继续SAT求解之前，针对BDD的开始来检查对切片变量的每个分配。

公开(公告)号：US08286137B2

公开(公告)日：2012-10-09

申请号：US12054575

申请日：2008-03-25

申请人： Vineet Kahlon ,  Aarti Gupta

发明人： Vineet Kahlon ,  Aarti Gupta

IPC分类号： G06F9/44

CPC分类号： G06F11/3608

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

摘要翻译： 用于通过并发程序中的模型检查进行程序验证的系统和方法包括将多个程序线程中的每一个建模为电路模型，并且通过组合包括执行程序的同步执行的约束的电路模型来生成整个程序的全电路 线程。 该程序使用同步执行进行验证，以减少验证程序所需的内存量以及为揭示错误而采取的一些步骤。

公开(公告)号：US08266600B2

公开(公告)日：2012-09-11

申请号：US11277401

申请日：2006-03-24

申请人： Vineet Kahlon ,  Aarti Gupta

发明人： Vineet Kahlon ,  Aarti Gupta

IPC分类号： G06F9/44

CPC分类号： G06F11/3608

摘要： A technique for model checking of multi-threaded software is herein disclosed which advantageously can be used to verify correctness properties expressed using temporal logic, e.g., linear time temporal logic and branching time temporal logic. The model checking problem of a concurrent system is decomposed into a plurality of model checking problems on individual threads of the multi-threaded software.

摘要翻译： 本文公开了一种用于多线程软件的模型检查的技术，其有利地可用于验证使用时间逻辑（例如线性时间逻辑和分支时间时间逻辑）表达的正确性属性。 并发系统的模型检查问题被分解为多线程软件的各个线程上的多个模型检查问题。

公开(公告)号：US07784035B2

公开(公告)日：2010-08-24

申请号：US11174791

申请日：2005-07-05

申请人： Vineet Kahlon ,  Aarti Gupta

发明人： Vineet Kahlon ,  Aarti Gupta

IPC分类号： G06F9/45

CPC分类号： G06F9/52 ,  G06F11/3608

摘要： A method for the static analysis of concurrent multi-threaded software which bypasses the state explosion situation that plagues the prior art, thereby making our method scalable while—at the same time—producing no loss in precision. Our inventive method maintains patterns of lock acquisition and lock release by individual threads by constructing augmented versions of the threads. Once the augmented versions have been constructed, our inventive method verifies the concurrent program using existing tools for the verification of sequential programs—thereby greatly reducing implementation overhead. Finally, our inventive augmentation and method is carried out in an automatic manner—without requiring user intervention.

摘要翻译： 一种用于并发多线程软件的静态分析方法，绕过了现有技术的状态爆炸情况，从而使我们的方法可扩展，同时产生精度上的损失。 本发明的方法通过构造线程的扩展版本来维护单独线程的锁获取和锁定释放模式。 一旦增强版本被构建，我们的创造性方法使用现有工具来验证并发程序来验证顺序程序，从而大大降低了实现开销。 最后，我们的创造性增加和方法是以自动的方式进行的 - 不需要用户干预。

公开(公告)号：US20090222249A1

公开(公告)日：2009-09-03

申请号：US12395955

申请日：2009-03-02

申请人： Chao Wang ,  Fang Yu ,  Aarti Gupta

发明人： Chao Wang ,  Fang Yu ,  Aarti Gupta

IPC分类号： G06F17/50

CPC分类号： G06F11/3608

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

摘要翻译： 用于验证分布式系统中的交互服务的组合的系统和方法包括为系统中的进程生成并行进程图（CPG），并对每个进程的CPG进行符号编码以执行可达性分析。 基于可达性分析，为同时运行的进程生成符号摘要。 通过利用过程的符号摘要来验证相关过程的系统来进行模块化验证。