What is Yices?
- 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 Web Interface
Yices Java API Lite
We developed a Yices Java API Lite to call Yices from a Java program. The API, documentation on installation and use of the API and an example are here.
Yices-Rainbow Eclipse Plugin
We developed an Eclipse Plugin called Yices-Rainbow to use Yices with the Eclipse IDE.