swMATH ID: 8528
Software Authors: Li, Yi; Albarghouthi, Aws; Kincaid, Zachary; Gurfinkel, Arie; Chechik, Marsha
Description: Symbolic optimization with SMT solvers. 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.
Homepage: http://dl.acm.org/citation.cfm?id=2535857
Keywords: invariant generation; optimization; program analysis; satisfiability modulo theories; symbolic abstraction
Related Software: z3; vZ; OptiMathSAT; MathSAT5; LogMIP; Yices; MiniSat; SMT-LIB; BioNetGen; Bio-PEPA; PRISM; Chaff; CVC4; STP; UppSAT; Boolector; KeY-ABS; Algorithm 864; Zephyrus2; SACO
Cited in: 13 Documents

Citations by Year