Program analysis via satisfiability modulo path programs

William R. Harris, Sriram Sankaranarayanan, Franjo Ivaňcíc, Aarti Gupta

Research output: Contribution to journalArticle

5 Scopus citations

Abstract

Path-sensitivity is often a crucial requirement for verifying safety properties of programs. As it is infeasible to enumerate and analyze each path individually, analyses compromise by soundly merging information about executions along multiple paths. However, this frequently results in a loss of precision. We present a program analysis technique that we call SatisfiabilityModulo Path Programs (SMPP), based on a path-based decomposition of a program. It is inspired by insights that have driven the development of modern SMT (Satisfiability Modulo Theory) solvers. SMPP symbolically enumerates path programs using a SAT formula over control edges in the program. Each enumerated path program is verified using an oracle, such as abstract interpretation or symbolic execution, to either find a proof of correctness or report a potential violation. If a proof is found, then SMPP extracts a sufficient set of control edges and corresponding interference edges, as a form of proof-based learning. Blocking clauses derived from these edges are added back to the SAT formula to avoid enumeration of other path programs guaranteed to be correct, thereby improving performance and scalability. We have applied SMPP in the F-Soft program verification framework, to verify properties of real-world C programs that require path-sensitive reasoning. Our results indicate that the precision from analyzing individual path programs, combined with their efficient enumeration by SMPP, can prove properties as well as indicate potential violations in the large.

Original languageEnglish (US)
Pages (from-to)71-81
Number of pages11
JournalACM SIGPLAN Notices
Volume45
Issue number1
DOIs
StatePublished - Jan 2010
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Keywords

  • Abstract Interpretation
  • Path Programs
  • Program Analysis
  • SATisfiability Solvers
  • SMT solvers
  • Symbolic Execution

Fingerprint Dive into the research topics of 'Program analysis via satisfiability modulo path programs'. Together they form a unique fingerprint.

  • Cite this