GO TO YICES OFFICIAL HOME PAGE
Yices is a decision procedure developed at SRI International that decides formulas in a combination of useful theories. Yices decides the satisfiability of formulas in a quantifier-free, first-order theory containing both uninterpreted function symbols and interpreted symbols from a rich combination including: real and integer arithmetic, recursive datatypes, tuples/records, extensional arrays, and lambda expressions. Yices supports a richer input language similar to the SAL language. Dependent types are also supported, since we found them to be useful for specifying properties of uninterpreted function symbols. Yices is still a prototype, we plan to release the system in 2006.
Yices got the first place in the QF_LIA (linear integer arithmetic) and QF_AUFLIA (arrays, uninterpreted functions, and linear integer arithmetic) divisions, and the second place in all other divisions in SMT-COMP'05.
Last modified: