The YICES SMT Solver

By Bruno Dutertre, Leonardo de Moura. 2006

727 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/0e55f506cbd6ecf3a44716cba7bc6f127904eaa8

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

1. Vijay Victor D'Silva
2. Georg Weissenbacher
3. Daniel Kroening
4. Wilfried Steiner
5. Tim King
6. Armando Solar-Lezama

Citations in the corpus

• An Evaluation of SMT-Based Schedule Synthesis for Time-Triggered Multi-hop Networks (2010, methodology): “We evaluate the performance of the state-ofthe-art SMT solver YICES [13] in the schedule synthesis using the defined formal schedule constraints and show that YICES out-of-the-box is capable of scheduling a TTEthernet network with hundreds of frame instances.”
• A Survey of Automated Techniques for Formal Software Verification (2008, methodology): “[6] A. Armando, J. Mantovani, and L. Platania, “Bounded model checking of software using SMT solvers instead of SAT solvers,” in Model Checking and Software Verification (SPIN), vol. 3925.”
• Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic (2014, methodology): “SMT solvers that have implemented this algorithm include Barcelogic [18], CVC4 [7], MathSAT [27], OpenSMT [23], SMTInterpol [26], Yices [48], Yices 2 [45], and Z3 [38].”