Advertisement

Abstract

Yices is an SMT solver developed by SRI International. The first version of Yices was released in 2006 and has been continuously updated since then. In 2007, we started a complete re-implementation of the solver to improve performance and increase modularity and flexibility. We describe the latest release of Yices, namely, Yices 2.2. We present the tool’s architecture and discuss the algorithms it implements, and we describe recent developments such as support for the SMT-LIB 2.0 notation and various performance improvements.

References

  1. 1.
    Shostak, R.E.: Deciding Combinations of Theories. In: Loveland, D.W. (ed.) CADE 1982. LNCS, vol. 138, pp. 209–222. Springer, Heidelberg (1982)CrossRefGoogle Scholar
  2. 2.
    Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol. 607, pp. 748–752. Springer, Heidelberg (1992)Google Scholar
  3. 3.
    Owre, S., Rushby, J., Shankar, N., von Henke, F.: Formal Verification of Fault-Tolerant Architectures: Prolegomena to the Design of PVS. IEEE Transactions on Software Engineering 21(2), 107–125 (1995)CrossRefGoogle Scholar
  4. 4.
    de Moura, L., Owre, S., Rueß, H., Rushby, J., Shankar, N.: The ICS Decision Procedures for Embedded Deduction. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol. 3097, pp. 218–222. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  6. 6.
    Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking. Journal of the ACM 52(3), 365–473 (2005)CrossRefMathSciNetGoogle Scholar
  7. 7.
    Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)CrossRefMATHGoogle Scholar
  8. 8.
    Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T.A., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient Satisfiability Modulo Theories via Delayed Theory Combination. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 335–349. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    de Moura, L., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  10. 10.
    Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  11. 11.
    Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013)Google Scholar
  12. 12.
    Bouton, T., de Oliveira, D.C.B., Déharbe, D., Fontaine, P.: veriT: An Open, Trustable, and Efficient SMT Solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151–156. Springer, Heidelberg (2009)Google Scholar
  13. 13.
    Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An Interpolating SMT Solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248–254. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  14. 14.
    Dutertre, B.: Yices 2 Manual. Technical report, Computer Science Laboratory, SRI International, Included in the Yices 2 distribution (2014)Google Scholar
  15. 15.
    Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical report, SMT-LIB Initiative (2006), http://www.smtlib.org
  16. 16.
    Barrett, C., Sump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Technical report, SMT-LIB Initiative (2012), http://www.smtlib.org
  17. 17.
    Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-Guided Component-Based Program Synthesis. In: Kramer, J., Bishop, J., Devanbu, P.T., Uchitel, S. (eds.) Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering (ICSE), pp. 215–224. ACM (2010)Google Scholar
  18. 18.
    Taly, A., Gulwani, S., Tiwari, A.: Synthesizing Switching Logic using Constraint Solving. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 305–319. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  19. 19.
    Cheng, C.H., Shankar, N., Rueß, H., Bensalem, S.: EFSMT: A Logical Framework for Cyber-Physical Systems. arXiv:1306:3456b2 (June 2014), http://www6.in.tum.de/~chengch/efsmt/
  20. 20.
    Eén, N., Sörensson, N.: An Extensible SAT Solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  21. 21.
    Biere, A.: PicoSAT Essentials. Journal on Satisfiability, Boolean Modelling, and Computation (JSAT) 4, 75–97 (2008)MATHGoogle Scholar
  22. 22.
    Nieuwenhuis, R., Oliveras, A.: Fast Congruence Closure and Extensions. Information and Computation 205(4), 557–580 (2007)CrossRefMATHMathSciNetGoogle Scholar
  23. 23.
    Dutertre, B., de Moura, L.: The Yices SMT Solver (2006), http://yices.csl.sri.com/tool-paper.pdf
  24. 24.
    de Moura, L., Bjørner, N.: Model-Based Theory Combination. Electronic Notes on Theoretical Computer Science 198(2), 37–49 (2008)CrossRefGoogle Scholar
  25. 25.
    Déharbe, D., Fontaine, P., Merz, S., Woltzenlogel Paleo, B.: Exploiting Symmetry in SMT Problems. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 222–236. Springer, Heidelberg (2011)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Bruno Dutertre
    • 1
  1. 1.Computer Science LaboratorySRI InternationalMenlo ParkUSA

Personalised recommendations