公开(公告)号：US20130332906A1

公开(公告)日：2013-12-12

申请号：US13874702

申请日：2013-05-01

申请人： Niloofar Razavi ,  Franjo Ivancic ,  Vineet Kahlon ,  Aarti Gupta

发明人： Niloofar Razavi ,  Franjo Ivancic ,  Vineet Kahlon ,  Aarti Gupta

IPC分类号： G06F11/36

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

摘要： A method to test a concurrent program by performing a concolic multi-trace analysis (CMTA) to analyze the concurrent program by taking two or more test runs over many threads and generating a satisfiability modulo theory (SMT) formula to select alternate inputs, alternate schedules and parts of threads from one or more test runs; using an SMT solver on the SMT formula for generating a new concurrent test comprising input values, thread schedules and parts of thread selections; and executing the new concurrent test.

摘要翻译： 通过执行多项多轨迹分析（CMTA）来测试并发程序的方法，通过在许多线程上进行两次或多次测试运行来分析并发程序，并生成可满足的模理论（SMT）公式来选择替代输入，替代计划 和来自一个或多个测试运行的线程的部分; 在SMT公式上使用SMT求解器生成新的并发测试，包括输入值，线程计划和线程选择的部分; 并执行新的并发测试。

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

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

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

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

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

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

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

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

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

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

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

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

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

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