Exploiting traces in static program analysis: Better model checking through printfs

Alex Groce, Rajeev Joshi

Research output: Contribution to journalArticlepeer-review

2 Scopus citations


From operating systems and web browsers to spacecraft, many software systems maintain a log of events that provides a partial history of execution, supporting post-mortem (or post-reboot) analysis. Unfortunately, bandwidth, storage limitations, and privacy concerns limit the information content of logs, making it difficult to fully reconstruct execution from these traces. This paper presents a technique for modifying a program such that it can produce exactly those executions consistent with a given (partial) trace of events, enabling efficient analysis of the reduced program. Our method requires no additional history variables to track log events, and it can slice away code that does not execute in a given trace. We describe initial experiences with implementing our ideas by extending the CBMC bounded model checker for C programs. Applying our technique to a small, 400-line file system written in C, we get more than three orders of magnitude improvement in running time over a naïve approach based on adding history variables, along with fifty- to eighty-fold reductions in the sizes of the SAT problems solved.

Original languageEnglish (US)
Pages (from-to)131-144
Number of pages14
JournalInternational Journal on Software Tools for Technology Transfer
Issue number2
StatePublished - Mar 2008
Externally publishedYes

ASJC Scopus subject areas

  • Software
  • Information Systems


Dive into the research topics of 'Exploiting traces in static program analysis: Better model checking through printfs'. Together they form a unique fingerprint.

Cite this