Yi Li
Aws Albarghouthi
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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.
Supplemental Material
- Competition On Software Verification - (SV-COMP). http://sv-comp.sosy-lab.org.Google Scholar
- Yices SMT Solver. http://yices.csl.sri.com.Google Scholar
- Z3 Source Code Repository. http://z3.codeplex.com/.Google Scholar
- A. Albarghouthi and K. L. McMillan. Beautiful Interpolants. In Proc. of CAV'13, pages 313--329, 2013. Google ScholarDigital Library
- A. Albarghouthi, A. Gurfinkel, and M. Chechik. UFO: A Framework for Abstraction- and Interpolation-Based Software Verification. In Proc. of CAV'12, pages 672--678, 2012. Google ScholarDigital Library
- E. Balas. Disjunctive programming: Properties of the convex hull of feasible points. Discrete Applied Mathematics, 89(1-3):3--44, 1998. Google ScholarDigital Library
- T. Ball and S. Rajamani. The SLAM Toolkit. In Proc. of CAV'01, volume 2102 of LNCS, pages 260--264, 2001. Google ScholarDigital Library
- C. Barrett, A. Stump, and C. Tinelli. The SMT-LIB Standard: Version 2.0. Technical report, Department of Computer Science, The University of Iowa, 2010. Available at www.SMT-LIB.org.Google Scholar
- C. Barrett, C. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, and C. Tinelli. CVC4. In Proc. of CAV'11, pages 171--177, 2011. Google ScholarDigital Library
- C.W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In Handbook of Satisfiability, pages 825--885. 2009.Google Scholar
- P. Barth. A Davis-Putnam based enumeration algorithm for linear pseudo-Boolean optimization. Technical Report MPI-I-95-2-003, Max-Planck-Institute für Informatik, 1995.Google Scholar
- D. Beyer, A. Cimatti, A. Griggio, M. E. Keremoglu, and R. Sebastiani. Software Model Checking via Large-Block Encoding. In Proc. of FMCAD'09, pages 25--32, 2009.Google ScholarCross Ref
- G. M. Bierman, A. D. Gordon, C. Hritcu, and D. E. Langworthy. Semantic Subtyping with an SMT Solver. J. Funct. Program., 22(1): 31--105, 2012. Google ScholarDigital Library
- N. Bjorner, K. McMillan, and A. Rybalchenko. Program Verification as Satisfiability Modulo Theories. In Proc. of SMT'12, 2012.Google Scholar
- C. Cadar, D. Dunbar, and D. R. Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proc. of OSDI'08, pages 209--224, 2008. Google ScholarDigital Library
- A. Chaganty, A. Lal, A. Nori, and S. Rajamani. Combining Relational Learning with SMT Solvers using CEGAR. In Proc. of CAV'13, pages 447--462, 2013. Google ScholarDigital Library
- A. Cimatti, A. Franzén, A. Griggio, R. Sebastiani, and C. Stenico. Satisfiability Modulo the Theory of Costs: Foundations and Applications. In Proc. of TACAS'10, pages 99--113, 2010. Google ScholarDigital Library
- A. Cimatti, A. Griggio, B. J. Schaafsma, and R. Sebastiani. The MathSAT5 SMT Solver. In Proc. of TACAS'13, pages 93--107, 2013. Google ScholarDigital Library
- E. Clarke, D. Kroening, and F. Lerda. A Tool for Checking ANSI-C Programs. In Proc. of TACAS'04, volume 2988 of LNCS, pages 168--176, March 2004.Google Scholar
- P. Cousot and R. Cousot. Static Determination of Dynamic Properties of Programs. In Proc. of the Colloque sur la Programmation, 1976.Google Scholar
- P. Cousot and R. Cousot. Abstract Interpretation: A Unified Lattice Model For Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proc. of POPL'77, pages 238--252, 1977. Google ScholarDigital Library
- L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In Proc. of TACAS'08, LNCS, pages 337--340, 2008. Google ScholarDigital Library
- R. DeLine and K. R. M. Leino. BoogiePL: A Typed Procedural Language for Checking Object-oriented Programs. Technical report, Microsoft Research, 2005.Google Scholar
- B. Dutertre and L. de Moura. A Fast Linear-Arithmetic Solver for DPLL(T). In Proc. of CAV'06, pages 81--94, 2006. Google ScholarDigital Library
- S. Falke, F. Merz, and C. Sinz. LLBMC: Improved Bounded Model Checking of C Programs Using LLVM. In Proc. of TACAS'13, pages 623--626, 2013. Google ScholarDigital Library
- H. Ganzinger, G. Hagen, R. Nieuwenhuis, A. Oliveras, and C. Tinelli. DPLL(T): Fast Decision Procedures. In Proc. of CAV'04, LNCS, pages 175--188, 2004.Google ScholarCross Ref
- P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In Proc. of PLDI'05, pages 213--223, 2005. Google ScholarDigital Library
- P. Godefroid, M. Y. Levin, and D. A. Molnar. SAGE: Whitebox Fuzzing for Security Testing. Commun. ACM, 55(3):40--44, 2012. Google ScholarDigital Library
- R. E. Gomory. Outline of an Algorithm for Integer Solutions to Linear Programs. Bull. Amer. Math. Soc., 64(5):275--278, 1958.Google ScholarCross Ref
- S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing Software Verifiers from Proof Rules. In Proc. of PLDI'12, pages 405--416, 2012. Google ScholarDigital Library
- S. Gulwani, S. Jha, A. Tiwari, and R. Venkatesan. Synthesis of Loop-Free Programs. In Proc. of PLDI'11, pages 62--73, 2011. Google ScholarDigital Library
- A. Gupta, C. Popeea, and A. Rybalchenko. Solving Recursion-Free Horn Clauses over LI+UIF. In Proc. of APLAS'11, pages 188--203, 2011. Google ScholarDigital Library
- A. Gurfinkel, S. Chaki, and S. Sapra. Efficient Predicate Abstraction of Program Summaries. In Proc. of NFM'11, volume 6617 of LNCS, pages 131--145, 2011. Google ScholarDigital Library
- W. R. Harris, S. Sankaranarayanan, F. Ivancic, and A. Gupta. Program Analysis via Satisfiability Modulo Path Programs. In Proc. of POPL'10, pages 71--82, 2010. Google ScholarDigital Library
- T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy Abstraction. In Proc. of POPL'02, pages 58--70, 2002. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from Proofs. In Proc. of POPL'04, pages 232--244, 2004. Google ScholarDigital Library
- S. Jha, S. Gulwani, S. A. Seshia, and A. Tiwari. Oracle-Guided Component-Based Program Synthesis. In Proc. of ICSE'10, pages 215--224, 2010. Google ScholarDigital Library
- A. S. Köksal, V. Kuncak, and P. Suter. Constraints as Control. In Proc. of POPL'12, pages 151--164, 2012. Google ScholarDigital Library
- K. R. M. Leino. Dafny: An Automatic Program Verifier for Functional Correctness. In Proc. of LPAR'10, pages 348--370, 2010. Google ScholarDigital Library
- A. Makhorin. The GNU Linear Programming Kit. http://www.gnu.org/software/glpk/, 2000.Google Scholar
- H. Massalin. Superoptimizer: a Look at the Smallest Program. SIGARCH Comput. Archit. News, 15(5):122--126, Oct. 1987. Google ScholarDigital Library
- A. Miné. The Octagon Abstract Domain. J. Higher-Order and Symbolic Computation, 19(1):31--100, 2006. Google ScholarDigital Library
- T. M. Mitchell. Machine Learning. McGraw-Hill, Inc., New York, NY, USA, 1997. Google ScholarDigital Library
- D. Monniaux. Automatic Modular Abstractions for Linear Constraints. In Proc. of POPL'09, pages 140--151, 2009. Google ScholarDigital Library
- D. Monniaux. Automatic Modular Abstractions for Template Numerical Constraints. Logical Methods in Computer Science, 6(3), 2010.Google Scholar
- R. Nieuwenhuis and A. Oliveras. On SAT Modulo Theories and Optimization Problems. In Proc. of SAT'06, pages 156--169, 2006. Google ScholarDigital Library
- F. Niu, C. Ré, A. Doan, and J. Shavlik. Tuffy: Scaling Up Statistical Inference in Markov Logic Networks Using an RDBMS. Proc. of VLDB'11, pages 373--384, 2011. Google ScholarDigital Library
- R. Piskac, T. Wies, and D. Zufferey. Automating Separation Logic using SMT. In Proc. of CAV'13, 2013. Google ScholarDigital Library
- J. C. Platt. Fast Training of Support Vector Machines Using Sequential Minimal Optimization. In Advances in Kernel Methods, pages 185--208. MIT Press, 1999. Google ScholarDigital Library
- R. Raman and I. Grossmann. Modelling and Computational Techniques for Logic Based Integer Programming. Computers and Chemical Engineering, 18(7):563--578, 1994.Google ScholarCross Ref
- T. Reps, M. Sagiv, and G. Yorsh. Symbolic Implementation of the Best Transformer. In Proc. of VMCAI'04, volume 2937 of LNCS, 2004.Google Scholar
- P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid Types. In Proc. of PLDI'08, pages 159--169, 2008. Google ScholarDigital Library
- A. Rybalchenko and V. Sofronie-Stokkermans. Constraint Solving for Interpolation. J. Symb. Comput., 45(11):1212--1233, 2010. Google ScholarDigital Library
- S. Sankaranarayanan, H. B. Sipma, and Z. Manna. Scalable Analysis of Linear Systems using Mathematical Programming. In Proc. of VMCAI'05, pages 25--41, 2005. Google ScholarDigital Library
- N.W. Sawaya and I. E. Grossmann. A Cutting Plane Method for Solving Linear Generalized Disjunctive Programming Problems. Computers And Chemical Engineering, 29(9):1891--1913, 2005.Google ScholarCross Ref
- R. Sebastiani and S. Tomasi. Optimization in SMT with LA(Q) Cost Functions. In Proc. of IJCAR'12, pages 484--498, 2012. Google ScholarDigital Library
- M. Sheeran and G. Ståmarck. A Tutorial on Stålmarck's Proof Procedure for Propositional Logic. FMSD, 16:23--58, 2000. Google ScholarDigital Library
- A. Solar-Lezama, L. Tancau, R. Bodík, S. A. Seshia, and V. A. Saraswat. Combinatorial Sketching for Finite Programs. In Proc. of ASPLOS'06, pages 404--415, 2006. Google ScholarDigital Library
- A. V. Thakur and T. W. Reps. A Method for Symbolic Computation of Abstract Operations. In Proc. of CAV'12, pages 174--192, 2012. Google ScholarDigital Library
- A. V. Thakur, M. Elder, and T. W. Reps. Bilateral Algorithms for Symbolic Abstraction. In Proc. of SAS'12, pages 111--128, 2012. Google ScholarDigital Library
- R. Wunderling. Paralleler und Objekt-orientierter Simplex-Algorithmus. PhD thesis, Technische Universität Berlin, 1996.Google Scholar
- D. Monniaux and L. Gonnord. Using Bounded Model Checking to Focus Fixpoint Iterations. In Proc. of SAS'11, pages 369--385, 2011. Google ScholarDigital Library
Index Terms
- Symbolic optimization with SMT solvers
Recommendations
Symbolic optimization with SMT solvers
POPL '14: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesThe 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 ...
Approximating Quantified SMT-Solving with SAT
SSIRI-C '11: Proceedings of the 2011 Fifth International Conference on Secure Software Integration and Reliability Improvement - CompanionSatisfiability Modulo Theories (SMT) is an extension of SAT towards FOL. SMT solvers have proven highly scalable and efficient for problems based on some ground theorems. However, SMT problems involving quantifiers and combination of theorems is a long-...
JavaSMT 3: Interacting with SMT Solvers in Java
Computer Aided VerificationAbstractSatisfiability Modulo Theories (SMT) is an enabling technology with many applications, especially in computer-aided verification. Due to advances in research and strong demand for solvers, there are many SMT solvers available. Since different ...
Comments