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

30 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 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
Pages71-81
Number of pages11
DOIs
StatePublished - Apr 20 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

Other

Other37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'10
CountrySpain
CityMadrid
Period1/17/101/23/10

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Abstract interpretation
  • Path sensitivity
  • Program analysis
  • SMT solvers
  • Satisfiability 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

    Harris, W. R., Sankaranarayanan, S., Ivančić, F., & Gupta, A. (2010). Program analysis via satisfiability modulo path programs. In POPL'10 - Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 71-81). (Conference Record of the Annual ACM Symposium on Principles of Programming Languages). https://doi.org/10.1145/1706299.1706309