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 cycle-accurate debugger with model checking algorithms provides an accurate model of software execution at the machine-code level while supporting concurrency 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.

Pdf version or through SpringerLink.

E. G. Mercer and M. D. Jones. “Model Checking Machine Code with the GNU Debugger,” Lecture Notes in Computer Science, vol. 3639, pages 251–256, August 2005.

@InProceedings{mercer:spin05,
  author =   {E.~G.~Mercer and M.~Jones},
  title =   {Model Checking Machine Code with the {GNU} Debugger},
  booktitle =  {12th International {SPIN} Workshop},
  year =  {2005},
  address =  {San Francisco, USA},
  month =  {August},
  OPTorganization = {},
  publisher =  {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3639}, 
  OPTnote =   {},
  pages = {251--265},
  annote =  {\input{mercer:spin05}}
}