Generating sound and effective memory debuggers

Yan Wang, Iulian Neamtiu, Rajiv Gupta

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations


We present a new approach for constructing debuggers based on declarative specification of bug conditions and root causes, and automatic generation of debugger code. We illustrate our approach on several classes of bugs, memory or otherwise. For each bug class, bug conditions and their root cause are specified declaratively, in First-order logic, using 1 to 4 predicates. We employ a low-level operational semantics and abstract traces to permit concise bug specification and prove soundness. To facilitate locating bugs, we introduce a new concept of value propagation chains that reduce programmer burden by narrowing the fault to a handful of executed instructions (1 to 16 in our experiments). We employ automatic translation to generate the debugger implementation, which runs on top of the Pin infrastructure. Experiments with using our system on 7 versions of 4 real-world programs show that our approach is expressive, effective at finding bugs and their causes, and efficient. We believe that, using our approach, other kinds of declaratively-specified, provably-correct, auto-generated debuggers can be constructed with little effort.

Original languageEnglish (US)
Title of host publicationISMM 2013 - Proceedings of the ACM SIGPLAN International Symposium on Memory Management
Number of pages12
StatePublished - 2013
Externally publishedYes
EventACM SIGPLAN International Symposium on Memory Management, ISMM 2013 - Seattle, WA, United States
Duration: Jun 20 2013Jun 20 2013

Publication series

NameInternational Symposium on Memory Management, ISMM


OtherACM SIGPLAN International Symposium on Memory Management, ISMM 2013
Country/TerritoryUnited States
CitySeattle, WA

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Software


  • Debugging
  • Fault localization
  • Logic specification
  • Operational semantics
  • Runtime monitoring


Dive into the research topics of 'Generating sound and effective memory debuggers'. Together they form a unique fingerprint.

Cite this