Model Checking Machine Code with the GNU Debugger

10 years 7 months ago
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.
Eric Mercer, Michael Jones
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where SPIN
Authors Eric Mercer, Michael Jones
Comments (0)