Model Checking Machine Code with the GNU Debugger

Embedded software verification is an important verification problem that requires the ability to reason about the timed semantics of concurrent behaviors at a low level of atomicity. The level of atomicity is the smallest execution block (such as a machine instruction or a C instruction) that cannot be split by an interrupt. Combining a cycleaccurate debugger with model checking algorithms provides an accurate model of software execution at the machine-code level while supporting ncy and allowing abstractions to manage state explosion. We report on the design and implementation of such a model checker using the GNU debugger (gdb) with different processor backends. A significant feature of the resulting tool is that we can adjust the level of atomicity during the model checking run to reduce state explosion while focusing on behaviors that are likely to generate an error.

• Type: Conference
• Year: 2005
• Where: SPIN
• Authors: Eric Mercer, Michael Jones
• Keywords: Model Checking, Model Checking Algorithms, SPIN 2005, State Explosion, Theoretical Computer Science