专利快速检索-快速检索全球专利，免费商用专利数据库-IPRDB

1. 发明授权

US07526750B2 Object-based systematic state space exploration of software 失效
标题翻译：基于对象的系统状态空间探索软件
公开(公告)号：US07526750B2
公开(公告)日：2009-04-28
申请号：US10778969
申请日：2004-02-13
申请人： Anthony D. Andrews , Shaz Qadeer , Niels Jakob Rehof , Sriram K. Rajamani , Yichen Xie
发明人： Anthony D. Andrews , Shaz Qadeer , Niels Jakob Rehof , Sriram K. Rajamani , Yichen Xie
IPC分类号： G06F9/44 , G06F7/00
CPC分类号： G06F11/3608 , Y10S707/99944
摘要： The state space of modeled software can be explored using an object-based systematic state explorer. The object-based model can perform well even in light of the complexities of concurrent software. During state space exploration, differences between states can be stored instead of storing a complete copy of the state.
摘要翻译：可以使用基于对象的系统状态浏览器来探索建模软件的状态空间。基于对象的模型可以在并发软件的复杂性方面表现良好。在状态空间探索期间，可以存储状态之间的差异，而不是存储状态的完整副本。

2. 发明授权

US07555418B1 Procedure summaries for multithreaded software 有权
标题翻译：多线程软件的过程摘要
公开(公告)号：US07555418B1
公开(公告)日：2009-06-30
申请号：US10742695
申请日：2003-12-19
申请人： Shaz Qadeer , Niels Jakob Rehof , Sriram K. Rajamani
发明人： Shaz Qadeer , Niels Jakob Rehof , Sriram K. Rajamani
IPC分类号： G06F9/45
CPC分类号： G06F11/3608 , G06F8/433
摘要： Procedure summaries can be generated and used for multithreaded software. A set of actions for a software procedure can be identified as atomically modelable with respect to multithreaded execution of the software. Such actions can be considered a transaction and deemed to have occurred one after another without interruption by other threads. Thus, multithreaded execution of the software can be modeled to detect programming flaws. For example, reachability analysis can be used in concert with the procedure summaries to determine if specified invariants fail.
摘要翻译：可以生成过程摘要并用于多线程软件。关于软件的多线程执行，可以将软件过程的一组动作识别为可原子模拟的。这种行为可以被认为是交易，被认为是一个接一个地发生而不被其他线程中断。因此，可以对软件的多线程执行进行建模，以检测编程缺陷。例如，可以与过程摘要一起使用可达性分析，以确定指定的不变量是否失败。

3. 发明授权

US07779382B2 Model checking with bounded context switches 失效
标题翻译：使用有界的上下文切换进行模型检查
公开(公告)号：US07779382B2
公开(公告)日：2010-08-17
申请号：US11009752
申请日：2004-12-10
申请人： Niels Jakob Rehof , Shaz Qadeer
发明人： Niels Jakob Rehof , Shaz Qadeer
IPC分类号： G06F9/44 , G06F9/445 , G06F11/00 , G06F15/00
CPC分类号： G06F11/3608
摘要： Validity of one or more assertions for any concurrent execution of a plurality of software instructions with at most k−1 context switches can be determined. Validity checking can account for execution of the software instructions in an unbounded stack depth scenario. A finite data domain representation can be used. The software instructions can be represented by a pushdown system. Validity checking can account for thread creation during execution of the plurality of software instructions.
摘要翻译：可以确定用于任何并发执行多达k-1个上下文切换的多个软件指令的一个或多个断言的有效性。有效性检查可以解释在无限堆栈深度场景中执行软件指令。可以使用有限数据域表示。软件指令可以由下推系统表示。有效性检查可以解释执行多个软件指令期间的线程创建。

4. 发明授权

US07650595B2 Sound transaction-based reduction without cycle detection 有权
标题翻译：基于声音的基于事务的减少，无周期检测
公开(公告)号：US07650595B2
公开(公告)日：2010-01-19
申请号：US11119530
申请日：2005-04-29
申请人： Shaz Qadeer , Sriram K. Rajamani , Vladimir A. Levin , Robert Palmer
发明人： Shaz Qadeer , Sriram K. Rajamani , Vladimir A. Levin , Robert Palmer
IPC分类号： G06F9/44
CPC分类号： G06F8/433 , G06F8/456 , G06F11/3608
摘要： Described techniques and tools help model checking scale to large programs while reducing missed errors. In particular, described techniques and tools help reduce the state space of concurrent programs without depending on cycle detection and without scheduling execution of postponed threads at all cycles. For example, described techniques and tools use a type of partial-order reduction called transaction-based reduction to reduce program state space. Analysis is performed at commit points to determine whether to schedule delayed threads.
摘要翻译：描述的技术和工具可帮助模型检查大型程序的规模，同时减少错误的错误。特别地，所描述的技术和工具有助于减少并发程序的状态空间，而不依赖于周期检测，并且在所有周期内不执行延迟的线程。例如，所描述的技术和工具使用一种称为基于事务的减少的部分顺序减少来减少程序状态空间。分析在提交点执行，以确定是否计划延迟的线程。

5. 发明申请

US20050086648A1 Object-based systematic state space exploration of software 失效
标题翻译：基于对象的系统状态空间探索软件
公开(公告)号：US20050086648A1
公开(公告)日：2005-04-21
申请号：US10778969
申请日：2004-02-13
申请人： Anthony Andrews , Shaz Qadeer , Niels Rehof , Sriram Rajamani , Yichen Xie
发明人： Anthony Andrews , Shaz Qadeer , Niels Rehof , Sriram Rajamani , Yichen Xie
IPC分类号： G06F9/44
CPC分类号： G06F11/3608 , Y10S707/99944
摘要： The state space of modeled software can be explored using an object-based systematic state explorer. The object-based model can perform well even in light of the complexities of concurrent software. During state space exploration, differences between states can be stored instead of storing a complete copy of the state.
摘要翻译：可以使用基于对象的系统状态浏览器来探索建模软件的状态空间。基于对象的模型可以在并发软件的复杂性方面表现良好。在状态空间探索期间，可以存储状态之间的差异，而不是存储状态的完整副本。

6. 发明授权

US07926035B2 Testing multi-thread software using prioritized context switch limits 失效
标题翻译：使用优先级上下文切换限制测试多线程软件
公开(公告)号：US07926035B2
公开(公告)日：2011-04-12
申请号：US11739427
申请日：2007-04-24
申请人： Madanlal S. Musuvathi , Shaz Qadeer
发明人： Madanlal S. Musuvathi , Shaz Qadeer
IPC分类号： G06F9/44 , G06F9/445
CPC分类号： G06F11/3688
摘要： Testing multithreaded application programs for errors can be carried out in an efficient and productive manner at least in part by prioritizing thread schedules based on numbers of context switches between threads therein. In particular, each thread schedule in a multithreaded application program can be prioritized based on whether a given thread schedule has the same as or less than some maximum value. A model checker module can then iteratively execute thread schedules that fit within a given context switch maximum value, or a progressively higher value up to some limit. In one implementation, for example, the model checker module executes all thread schedules that have zero preempting context switches, then all thread schedules that have only one preempting context switch, etc. Most errors in an application program can be identified by executing only those thread schedule with relatively few preempting context switches.
摘要翻译：测试用于错误的多线程应用程序可以以有效和高效的方式进行，至少部分地基于基于线程之间的上下文切换的数量来优先考虑线程调度。具体来说，多线程应用程序中的每个线程调度可以基于给定的线程调度是否具有或小于某个最大值来确定优先级。然后，模型检查器模块可以迭代地执行适合给定上下文切换最大值的线程调度，或者达到某种限制的逐渐更高的值。在一个实现中，例如，模型检查器模块执行具有零抢占上下文切换的所有线程调度，然后仅具有一个抢占上下文切换的所有线程调度等。应用程序中的大多数错误可以通过仅执行那些线程来识别具有相对较少的抢占上下文切换的时间表。

7. 发明申请

US20130241941A1 STATIC VERIFICATION OF PARALLEL PROGRAM CODE 有权
标题翻译：并行程序代码的静态验证
公开(公告)号：US20130241941A1
公开(公告)日：2013-09-19
申请号：US13423255
申请日：2012-03-18
申请人： Alastair Francis Donaldson , Shaz Qadeer
发明人： Alastair Francis Donaldson , Shaz Qadeer
IPC分类号： G06F15/80 , G06F12/00 , G06F9/44
CPC分类号： G06F9/44589
摘要： A symbolic encoding of predicated execution for static verification, based on a plurality of data parallel program instructions, is obtained. A result of static verification of one or more attributes associated with the plurality of data parallel program instructions is obtained, based on the symbolic encoding.
摘要翻译：获得基于多个数据并行程序指令的用于静态验证的预定执行的符号编码。基于符号编码获得与多个数据并行程序指令相关联的一个或多个属性的静态验证的结果。

8. 发明授权

US09053227B2 Concurrent assertion 有权
标题翻译：同时断言
公开(公告)号：US09053227B2
公开(公告)日：2015-06-09
申请号：US13415854
申请日：2012-03-09
申请人： Jacob Samuels Burnim , Madanlal Musuvathi , Shaz Qadeer
发明人： Jacob Samuels Burnim , Madanlal Musuvathi , Shaz Qadeer
IPC分类号： G06F9/46 , G06F11/36 , G06F9/48
CPC分类号： G06F11/3604 , G06F9/4881 , G06F11/366
摘要： A concurrency assertions system disclosed herein provides for atomic evaluation of an assertion expression by locking an assertion lock upon initiating an assertion and thereby protecting the assertion evaluation from concurrent modifications to the variables in the assertion expressions. When a violation of an assertion is detected, the concurrency assertions system ensures that the exception statistics at the time of the assertion violation represents a program state where the assertion is violated, thus improving analysis of assertion violations. Furthermore, the concurrency assertions system continuously evaluates an expression for an assertion for a time period while other threads in the program are being executed.
摘要翻译：本文公开的并发断言系统提供了通过在发起断言时锁定断言锁定从而保护断言评估免于对断言表达式中的变量的并发修改来对断言表达式进行原子评估。当检测到断言的违反时，并发断言系统确保在断言违规时的异常统计信息表示违反断言的程序状态，从而改善断言违规的分析。此外，并发断言系统在执行程序中的其他线程的同时持续评估断言的表达式。

9. 发明申请

US20090178044A1 FAIR STATELESS MODEL CHECKING 有权
标题翻译：公平无缺陷模型检查
公开(公告)号：US20090178044A1
公开(公告)日：2009-07-09
申请号：US11971656
申请日：2008-01-09
申请人： Madanlal Musuvathi , Shaz Qadeer
发明人： Madanlal Musuvathi , Shaz Qadeer
IPC分类号： G06F9/46
CPC分类号： G06F9/4881 , G06F2209/484
摘要： Techniques for providing a fair stateless model checker are disclosed. In some aspects, a schedule is generated to allocate resources for threads of a multi-thread program in lieu of having an operating system allocate resources for the threads. The generated schedule is both fair and exhaustive. In an embodiment, a priority graph may be implemented to reschedule a thread when a different thread is determined not to be making progress. A model checker may then implement one of the generated schedules in the program in order to determine if a bug or a livelock occurs during the particular execution of the program. An output by the model checker may facilitate identifying bugs and/or livelocks, or authenticate a program as operating correctly.
摘要翻译：公开了提供公平无状态模型检查器的技术。在某些方面，生成一个调度表来为多线程程序的线程分配资源，代替具有为线程分配资源的操作系统。生成的时间表是公平和详尽的。在一个实施例中，当确定不同的线程不进行时，可以实现优先级图表来重新调度线程。然后，模型检查器可以在程序中实现所生成的计划之一，以便确定在程序的特定执行期间是否发生错误或活锁。模型检查器的输出可以有助于识别错误和/或活动锁定，或者将程序认证为正确操作。

10. 发明申请

US20070245312A1 Precise data-race detection using locksets 失效
标题翻译：使用锁具进行精确的数据竞赛检测
公开(公告)号：US20070245312A1
公开(公告)日：2007-10-18
申请号：US11403414
申请日：2006-04-12
申请人： Shaz Qadeer , Tayfun Elmas
发明人： Shaz Qadeer , Tayfun Elmas
IPC分类号： G06F9/44 , G06F9/45
CPC分类号： G06F11/3632
摘要： A data race detection system is described which precisely identifies data races in concurrent programs. The system and techniques described utilize locksets to maintain information while searching through executions of a concurrent program. The locksets are updated according to program statements in the concurrent program. The dynamic updating of the locksets, combined with a less conservative approach then used in existing lockset data race detection techniques, allows the technique to be precise; that is, the technique does not report false positives when searching a program.
摘要翻译：描述了数据竞争检测系统，其精确地识别并发程序中的数据竞赛。所描述的系统和技术利用锁定装置来维护信息，同时在执行并行程序的同时进行搜索。根据并发程序中的程序语句更新锁定。锁定器的动态更新与现有锁定数据种族检测技术中使用的较不保守的方法相结合，使得该技术是精确的; 也就是说，在搜索程序时，该技术不会报告错误的肯定。

你已经成功收藏专利！

检索式保存成功!

IPRDB

热门服务

关于我们

友情链接

联系方式