Yices

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

• You can try out Yices (1.0) using the Web interface we developed with some small examples available on the official Yices Web site.

• Access 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.