公开(公告)号：US08176496B2

公开(公告)日：2012-05-08

申请号：US12181665

申请日：2008-07-29

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

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

IPC分类号： G06F9/44 ,  G06F9/46 ,  G06F9/50

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

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

摘要翻译： 用于对并发系统进行符号部分顺序减少的系统和方法包括：当条件或谓词成立时，确定包括对于一组状态是独立的不同线程的转移的被保护的独立关系。 当保护的独立性条件成立时，使用保护的独立关系执行部分顺序减少以允许冗余线程交织的自动修剪。

公开(公告)号：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排序约束来选择高风险的交织以供将来测试执行。

公开(公告)号：US08136098B2

公开(公告)日：2012-03-13

申请号：US11777129

申请日：2007-07-12

申请人： Vineet Kahlon ,  Aarti Gupta

发明人： Vineet Kahlon ,  Aarti Gupta

IPC分类号： G06F9/44

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

摘要： A static, inter-procedural dataflow analysis is used to debug multi-threaded programs which heretofore have been thought unsuitable for concurrent multi-threaded analysis.

摘要翻译： 静态的程序间数据流分析用于调试以前被认为不适合并发多线程分析的多线程程序。

公开(公告)号：US20100205592A1

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

申请号：US12701962

申请日：2010-02-08

申请人： SRIRAM SANKARANARAYANAN ,  Aarti Gupta ,  Gogul Balakrishnan

发明人： SRIRAM SANKARANARAYANAN ,  Aarti Gupta ,  Gogul Balakrishnan

IPC分类号： G06F9/45

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.

摘要翻译： 描述了用于在软件程序中发现给定循环的一组可能的迭代序列的系统和方法，以变换循环表示。 在包含循环的程序中，基于分割标准将循环分成多个部分。 标签与这些部分相关联，并且构建了一个初始循环自动机，它将循环迭代表示为与程序中的部分相对应的标签上的常规语言。 分析标签的子序列，以确定自动机中允许的子序列的不可行性。 通过去除所有不可行子序列来发现循环中的一组可能的迭代序列来改进自动机。 所产生的循环自动机被用于随后的程序验证或分析技术中以发现程序中的正确性属性的违反。

公开(公告)号：US20080178156A1

公开(公告)日：2008-07-24

申请号：US11954869

申请日：2007-12-12

申请人： Vineet Kahlon ,  Yu Yang ,  Sriram Sankaranarayanan ,  Aarti Gupta

发明人： Vineet Kahlon ,  Yu Yang ,  Sriram Sankaranarayanan ,  Aarti Gupta

IPC分类号： G06F9/44

CPC分类号： G06F9/52 ,  G06F8/433 ,  G06F9/526

摘要： A system and method for race warning generation for computer program verification includes determining shared variables and determining context-sensitive points-to sets for lock pointers by focusing on pointers that may affect aliases of lock pointers, and by leveraging function summarization. Locksets are determined at locations where shared variables are accessed using the points-to sets for lock pointers. Warnings are based on disjointness of locksets.

摘要翻译： 用于计算机程序验证的用于赛跑警告生成的系统和方法包括通过关注可能影响锁定指针的别名的指针以及通过利用功能汇总来确定共享变量并且确定用于锁指针的上下文相关点集合。 使用锁定指针的点对集来访问共享变量的位置确定锁定。 警告是基于锁具的不相容性。

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

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

公开(公告)号：US08185875B2

公开(公告)日：2012-05-22

申请号：US11954869

申请日：2007-12-12

申请人： Vineet Kahlon ,  Yu Yang ,  Sriram Sankaranarayanan ,  Aarti Gupta

发明人： Vineet Kahlon ,  Yu Yang ,  Sriram Sankaranarayanan ,  Aarti Gupta

IPC分类号： G06F9/44

CPC分类号： G06F9/52 ,  G06F8/433 ,  G06F9/526

摘要： A system and method for race warning generation for computer program verification includes determining shared variables and determining context-sensitive points-to sets for lock pointers by focusing on pointers that may affect aliases of lock pointers, and by leveraging function summarization. Locksets are determined at locations where shared variables are accessed using the points-to sets for lock pointers. Warnings are based on disjointness of locksets.

摘要翻译： 用于计算机程序验证的用于赛跑警告生成的系统和方法包括通过关注可能影响锁定指针的别名的指针以及通过利用功能汇总来确定共享变量并且确定用于锁指针的上下文相关点集合。 使用锁定指针的点对集来访问共享变量的位置确定锁定。 警告是基于锁具的不相容性。

公开(公告)号：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求解器在并发程序的探索期间动态添加约束，以确保模型检查的准单调性。