Symbolic optimization with SMT solvers

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

Research output: Contribution to journalArticle

23 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)
Pages (from-to)607-618
Number of pages12
JournalACM SIGPLAN Notices
Volume49
Issue number1
StatePublished - Jan 13 2014
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

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