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.
This work was supported in part by DARPA under contract FA8750-12-C-0284 and by the NSF Grant SHF:CSR-1017483. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author and do not necessarily reflect the views of the funding agencies.
Chapter PDF
Similar content being viewed by others
References
Shostak, R.E.: Deciding Combinations of Theories. In: Loveland, D.W. (ed.) CADE 1982. LNCS, vol. 138, pp. 209–222. Springer, Heidelberg (1982)
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)
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)
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)
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)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking. Journal of the ACM 52(3), 365–473 (2005)
Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems 1(2), 245–257 (1979)
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)
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)
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)
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)
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)
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)
Dutertre, B.: Yices 2 Manual. Technical report, Computer Science Laboratory, SRI International, Included in the Yices 2 distribution (2014)
Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical report, SMT-LIB Initiative (2006), http://www.smtlib.org
Barrett, C., Sump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. Technical report, SMT-LIB Initiative (2012), http://www.smtlib.org
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)
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)
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/
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)
Biere, A.: PicoSAT Essentials. Journal on Satisfiability, Boolean Modelling, and Computation (JSAT) 4, 75–97 (2008)
Nieuwenhuis, R., Oliveras, A.: Fast Congruence Closure and Extensions. Information and Computation 205(4), 557–580 (2007)
Dutertre, B., de Moura, L.: The Yices SMT Solver (2006), http://yices.csl.sri.com/tool-paper.pdf
de Moura, L., Bjørner, N.: Model-Based Theory Combination. Electronic Notes on Theoretical Computer Science 198(2), 37–49 (2008)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Dutertre, B. (2014). Yices 2.2. In: Biere, A., Bloem, R. (eds) Computer Aided Verification. CAV 2014. Lecture Notes in Computer Science, vol 8559. Springer, Cham. https://doi.org/10.1007/978-3-319-08867-9_49
Download citation
DOI: https://doi.org/10.1007/978-3-319-08867-9_49
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08866-2
Online ISBN: 978-3-319-08867-9
eBook Packages: Computer ScienceComputer Science (R0)