Ethan A Burns

US Patent:

20130304755, Nov 14, 2013

Filed:

May 12, 2012

Appl. No.:

13/470280

Inventors:

Rong Zhou - San Jose CA, US
Ethan Burns - Dover NH, US

Assignee:

PALO ALTO RESEARCH CENTER INCORPORATED - Palo Alto CA

International Classification:

G06F 17/30

US Classification:

707758, 707E17009

Abstract:

A technique for parallelizing model checking using breadth-first search in order to detect deadlocks and safety property violations is disclosed. The technique is based on Parallel Structured Duplicate Detection (PSDD) and preserves a model checker's ability to perform partial order reduction with parallel breadth-first search. PSDD also uses much less memory and is able to achieve better parallel speedup and verify models more quickly. Also, PSDD used herein is able to make use of external memory, such as hard disks, to reduce the memory requirements of verification.