Accelerating model checking via synchrony
US8286137B2 · kind B2 · utility
13Cited by
16References
4Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Mar 25, 2008 |
| Grant date | Oct 9, 2012 |
| Priority date | — |
| Expiry date | Jul 5, 2031 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3608
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
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.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.