Symbolic optimization with SMT solvers

Yi Li, Aws Albarghouthi, Zachary Kincaid, Arie Gurfinkel, Marsha Chechik

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

47 Scopus citations

Abstract

The rise in efficiency of Satisfiability Modulo Theories (SMT) solvers has created numerous uses for them in software verification, program synthesis, functional programming, refinement types, etc. In all of these applications, SMT solvers are used for generating satisfying assignments (e.g., a witness for a bug) or proving unsatisfiability/validity(e.g., proving that a subtyping relation holds). We are often interested in finding not just an arbitrary satisfying assignment, but one that optimizes (minimizes/maximizes) certain criteria. For example, we might be interested in detecting program executions that maximize energy usage (performance bugs), or synthesizing short programs that do not make expensive API calls. Unfortunately, none of the available SMT solvers offer such optimization capabilities. In this paper, we present SYMBA, an efficient SMT-based optimization algorithm for objective functions in the theory of linear real arithmetic (LRA). Given a formula φ and an objective function t, SYMBA finds a satisfying assignment of φ that maximizes the value of t. SYMBA utilizes efficient SMT solvers as black boxes. As a result, it is easy to implement and it directly benefits from future advances in SMT solvers. Moreover, SYMBA can optimize a set of objective functions, reusing information between them to speed up the analysis. We have implemented SYMBA and evaluated it on a large number of optimization benchmarks drawn from program analysis tasks. Our results indicate the power and efficiency of SYMBA in comparison with competing approaches, and highlight the importance of its multi-objective-function feature.

Original languageEnglish (US)
Title of host publicationPOPL 2014 - Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages607-618
Number of pages12
DOIs
StatePublished - 2014
Externally publishedYes
Event41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 - San Diego, CA, United States
Duration: Jan 22 2014Jan 24 2014

Publication series

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

Other

Other41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014
CountryUnited States
CitySan Diego, CA
Period1/22/141/24/14

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • invariant generation
  • optimization
  • program analysis
  • satisfiability modulo theories
  • symbolic abstraction

Fingerprint Dive into the research topics of 'Symbolic optimization with SMT solvers'. Together they form a unique fingerprint.

  • Cite this

    Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., & Chechik, M. (2014). Symbolic optimization with SMT solvers. In POPL 2014 - Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 607-618). (Conference Record of the Annual ACM Symposium on Principles of Programming Languages). https://doi.org/10.1145/2535838.2535857