Home	•	Intro	•	Docs	•	Wiki	•	FAQ	•	Download	-	Mail	•	Awards	•	Status	•	FM Tools

Yices: An SMT Solver

Please see the preliminary notice about AFM08 -- a workshop for PVS, SAL and Yices users *NEW*

Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixed-size bit-vectors, quantifiers, and lambda expressions. Yices also does MaxSMT (and, dually, unsat cores) and is competitive as an ordinary SAT and MaxSAT solver.

Introduction
Documentation
Wiki
FAQ (Frequently Asked Questions)
Download
Yices is available as a free binary download for many platforms; we do not currently provide source. If you would like to discuss alternative license terms, please contact fm-licensing@csl.sri.com.
Mailing Lists and Bug Reports
Awards
Status

Yices is one of the SRI FormalWare tools.

Home	•	Intro	•	Docs	•	Wiki	•	FAQ	•	Download	-	Mail	•	Awards	•	Status	•	FM Tools

Last modified: Tue 22 Jan 2008 17:08 PST