Invention Grant
US08448145B2 Methods and systems for reducing verification conditions for concurrent programs using mutually atomic transactions
有权
用于减少使用相互原子交易的并发程序的验证条件的方法和系统
- Patent Title: Methods and systems for reducing verification conditions for concurrent programs using mutually atomic transactions
- Patent Title (中): 用于减少使用相互原子交易的并发程序的验证条件的方法和系统
-
Application No.: US12569557Application Date: 2009-09-29
-
Publication No.: US08448145B2Publication Date: 2013-05-21
- Inventor: Malay K. Ganai , Sudipta Kundu
- Applicant: Malay K. Ganai , Sudipta Kundu
- Applicant Address: US NJ Princeton
- Assignee: NEC Laboratories America, Inc.
- Current Assignee: NEC Laboratories America, Inc.
- Current Assignee Address: US NJ Princeton
- Agent Joseph Kolodka; James Bitetto
- Main IPC: G06F9/44
- IPC: G06F9/44
Abstract:
Methods and systems for generating verification conditions and verifying the correctness of a concurrent system of program threads are described. The methods and systems determine and employ mutually atomic transactions to reduce verification problem sizes and state space for concurrent systems. The embodiments provide both an adequate and an optimal set of token-passing constraints for a bounded unrolling of threads.
Public/Granted literature
Information query
