Accelerating model checking via synchrony

• US 8,286,137 B2
• Filed: 03/25/2008
• Issued: 10/09/2012
• Est. Priority Date: 05/07/2007
• Status: Active Grant

• Current Assignee: NEC Corporation
• Original Assignee: NEC Laboratories America Inc (NEC Corporation)
• Inventors: Kahlon, Vineet, Gupta, Aarti
• Primary Examiner(s): Das, Chameli
• Application Number:
  US12/054,575
• Publication Number:
  US 20080282221A1
• Time in Patent Office: 1,659 Days
• Field of Search: 717/124
• US Class Current: 717/126
• CPC Class Codes: G06F 11/3608 using formal methods, e.g. model checking, abstract interpretation theorem proving G06N5/013

Abstract

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.

Claims

1. A computer implemented method for program verification by via bounded or unbounded model checking in concurrent programs, comprising:

modeling each of a plurality of program threads as a circuit model;

generating a full circuit for an entire program by combining the circuit models including constraints which enforce synchronous execution of the program threads; and

verifying the program using the synchronous execution to reduce the amount of memory needed to verify the program and a number of steps taken to uncover an error;

wherein using the synchronous execution includes determining synchronous conflicts conflicts to determine the subset of transitions that must be explored from each global state.

2. The method as recited in claim 1, further comprising leveraging synchronous execution to reduce,the depth of computations explored during model checking.

3. The method as recited in claim 1, wherein verifying includes:

checking necessary interleavings induced by shared variable updates and synchronization primitives by switching from interleaving to synchronous semantics while preserving a temporal property being model checked; and

integrating synchronous execution with partial order reduction, transactions and symbolic model checking.

4. The method as recited in claim 1, wherein using the synchronous execution includes determining synchronous conflicts.