公开(公告)号：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）表示形式生成逻辑公式，包括至少一个断言属性或原子性冲突。 然后确定公式的可满足性，使得确定的结果表示断言/原子性违规。

公开(公告)号：US07386818B2

公开(公告)日：2008-06-10

申请号：US11037920

申请日：2005-01-18

申请人： Malay Ganai ,  Aarti Gupta ,  Pranav Ashar

发明人： Malay Ganai ,  Aarti Gupta ,  Pranav Ashar

IPC分类号： G06F17/50

CPC分类号： G11C29/54 ,  G06F17/504 ,  G11C2029/0401

摘要： A computer-implemented method for augmenting SAT-based BMC to handle embedded memory designs without explicitly modeling memory bits. As is known, verifying designs having large embedded memories is typically handled by abstracting out (over-approximating) the memories. Such abstraction is not useful for finding real bugs. SAT-based BMC, as of now, is incapable of handling designs with explicit memory modeling due to enormously increased search space complexity. Advantageously, our method does not require analyzing the designs and also guarantees not to generate false negatives.

摘要翻译： 一种用于增加基于SAT的BMC来处理嵌入式存储器设计而不明确建模存储器位的计算机实现的方法。 众所周知，验证具有大嵌入存储器的设计通常通过抽象出（过近似）存储器来处理。 这样的抽象对于找到真实的错误是没有用的。 目前，基于SAT的BMC由于搜索空间复杂度的大幅增加，无法处理具有显式内存建模的设计。 有利的是，我们的方法不需要分析设计，也不保证不产生假阴性。

公开(公告)号：US07203917B2

公开(公告)日：2007-04-10

申请号：US10795384

申请日：2004-03-09

申请人： Malay Ganai ,  Aarti Gupta ,  Zijiang Yang ,  Pranav Ashar

发明人： Malay Ganai ,  Aarti Gupta ,  Zijiang Yang ,  Pranav Ashar

IPC分类号： G06F17/50

CPC分类号： G06F17/504

摘要： There is provided a method of solving a SAT problem comprising partitioning SAT-formula clauses in the SAT problem into a plurality of partitions. Each of said plurality of partitions is solved as a separate process each, thereby constituting a plurality of processes where each of said process communicates only with a subset of the plurality of processes.

摘要翻译： 提供了一种解决SAT问题的方法，包括将SAT问题中的SAT公式子句分成多个分区。 所述多个分区中的每一个分别被解决为单独的处理，从而构成多个处理，其中每个所述进程仅与多个进程的子集进行通信。

公开(公告)号：US6035109A

公开(公告)日：2000-03-07

申请号：US847952

申请日：1997-04-22

申请人： Pranav N Ashar ,  Aarti Gupta ,  Sharad Malik

发明人： Pranav N Ashar ,  Aarti Gupta ,  Sharad Malik

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

CPC分类号： G06F17/504

摘要： The Complete-1-Distinguishability (C-1-D) property is used for simplifying FSM verification. This property eliminates the need for a traversal of the product machine for the implementation machine and the specification machine. Instead, a much simpler check suffices. This check consists of first obtaining a 1-equivalence mapping between the states of the two machines, and then checking that it is a bisimulation relation. The C-1-D property can be used directly on specifications for which it naturally holds. This property can be enforced on arbitrary FSMs by exposing some of the latch outputs as pseudo-primary outputs during synthesis and verification. In this sense, the synthesis/verification methodology provides another point in the tradeoff curve between constraints-on-synthesis versus complexity-of-verification.

摘要翻译： 完整的1分辨率（C-1-D）属性用于简化FSM验证。 该特性不需要对实施机器和规格机器的产品机器进行遍历。 相反，一个更简单的检查就足够了。 该检查包括首先在两台机器的状态之间获得1等效映射，然后检查它是否是双向关系。 C-1-D属性可以直接用于其自然拥有的规格。 通过在合成和验证期间将某些锁存输出作为伪主输出，可以在任意的FSM上强制实现该属性。 在这个意义上，综合/验证方法在合成约束与验证复杂度之间的权衡曲线中提供了另一个要点。

公开(公告)号：US08527976B2

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

申请号：US12241340

申请日：2008-09-30

申请人： Vineet Kahlon ,  Sriram Sankarnarayanan ,  Aarti Gupta

发明人： Vineet Kahlon ,  Sriram Sankarnarayanan ,  Aarti Gupta

IPC分类号： G06F9/45

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

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

摘要翻译： 用于程序验证的系统和方法包括为并发程序生成产品交易图，其捕获潜在错误的警告。 通过使用通过对并发程序执行一个或多个数据流分析方法派生的同步原语和不变量的约束来过滤警告以消除伪造警告。 数据流分析方法按照间接费用的顺序进行应用。 使用模型检查生成剩余警告的具体执行跟踪。

公开(公告)号：US07853906B2

公开(公告)日：2010-12-14

申请号：US11689803

申请日：2007-03-22

申请人： Malay Ganai ,  Aarti Gupta

发明人： Malay Ganai ,  Aarti Gupta

IPC分类号： G06F9/45 ,  G06F17/50

CPC分类号： G06F17/504

摘要： An accelerated High-Level Bounded Model Checking method that efficiently extracts high-level information from the model, uses that extracted information to obtain an improved verification model, and applies relevant information on-the-fly to simplify the BMC-problem instances.

摘要翻译： 一种从模型中有效提取高级别信息的加速高级有界模型检查方法，利用提取的信息获取改进的验证模型，并即时应用相关信息，简化BMC问题实例。

公开(公告)号：US07711525B2

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

申请号：US10157486

申请日：2002-05-30

申请人： Malay Ganai ,  Lintao Zhang ,  Aarti Gupta ,  Zijiang Yang ,  Pranav Ashar

发明人： Malay Ganai ,  Lintao Zhang ,  Aarti Gupta ,  Zijiang Yang ,  Pranav Ashar

IPC分类号： G06F17/10

CPC分类号： G06F17/504

摘要： A method for bounded model checking of arbitrary Linear Time Logic temporal properties. The method comprises translating properties associated with temporal operators F(p), G(p), U(p, q) and X(p) into property checking schemas comprising Boolean satisfiability checks, wherein F represents an eventuality operator, G represents a globally operator, U represents an until operator and X represents a next-time operator. The overall property is checked in a customized manner by repeated invocations of the property checking schemas for F(p), G(p), U(p, q), X(p) operators and standard handling of atomic propositions and Boolean operators.

摘要翻译： 一种用于任意线性时间逻辑时间属性的有界模型检查的方法。 该方法包括将与时间运算符F（p），G（p），U（p，q）和X（p）相关联的属性转换成包括布尔可满足性检查的属性检查模式，其中F表示可能性运算符，G表示全局 运算符，U表示直到运算符，X表示下一运算符。 通过重复调用F（p），G（p），U（p，q），X（p）运算符的属性检查模式以及原子命题和布尔运算符的标准处理来检查整体属性。

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