SYMBA 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; SMT-LIB; MiniSat; BioNetGen; Bio-PEPA; PRISM; Chaff; CVC4; STP; UppSAT; Boolector; Algorithm 864; Zephyrus2; KeY-ABS; SACO Cited in: 13 Publications all top 5 Cited by 35 Authors 3 Sebastiani, Roberto 2 Chen, Li 2 Lyu, Yinrun 2 Min-Allah, Nasro 2 Trentin, Patrick 2 Tribastone, Mirco 2 Vandin, Andrea 2 Wang, Yongji 2 Zhang, Changyou 1 Ábrahám, Erika 1 Albarghouthi, Aws 1 Alhiyafi, Jamal 1 Cardelli, Luca 1 Chechik, Marsha 1 Chen, Liqian 1 Eraşcu, Mădălina 1 Gurfinkel, Arie 1 Hyvärinen, Antti E. J. 1 Jiang, Jiahong 1 Kincaid, Zachary 1 Kremer, Gereon 1 Li, Yi 1 Marescotti, Matteo 1 Micota, Flavia 1 Passerini, Andrea 1 Qu, Dacheng 1 Shankar, Natarajan 1 Sharygina, Natasha 1 Teso, Stefano 1 Tschaikowski, Max 1 Wang, Chong 1 Wang, Ji 1 Wu, Jingzheng 1 Wu, Xueguang 1 Zaharie, Daniela Cited in 5 Serials 2 Journal of Automated Reasoning 2 Journal of Global Optimization 1 Artificial Intelligence 1 Theoretical Computer Science 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 6 Fields 11 Computer science (68-XX) 4 Operations research, mathematical programming (90-XX) 2 Mathematical logic and foundations (03-XX) 1 Ordinary differential equations (34-XX) 1 Biology and other natural sciences (92-XX) 1 Systems theory; control (93-XX) Citations by Year