Program analysis via satisfiability modulo path programs

William R. Harris, Sriram Sankaranarayanan, Franjo Ivančić, Aarti Gupta

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

34 Scopus citations


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 Satisfiability Modulo 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)
Title of host publicationPOPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Number of pages11
StatePublished - 2010
Externally publishedYes
Event37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10 - Madrid, Spain
Duration: Jan 17 2010Jan 23 2010

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566


Other37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10

All Science Journal Classification (ASJC) codes

  • Software


  • Abstract interpretation
  • Path sensitivity
  • Program analysis
  • SMT solvers
  • Satisfiability solvers
  • Symbolic execution


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

Cite this