Main Page

This is the root of the Wiki pages for the Yices SMT solver.

The Yices static web pages are here.

Wikis for our other systems are here: PVS, SAL; and here's our top-level wiki: Formal Methods at SRI.

The purpose of this Wiki is to allow more comprehensive and uptodate dissemination of information relating to Yices by allowing anybody to edit and contribute to these pages. You are encouraged to join in--please make sure your content is relevant to Yices. We are using the MediaWiki software (same as Wikipedia). Click on 'Help' button on the left for using the Wiki.

Contents 1 Documentation and Help 2 News and Plans 3 SMT Competitions 4 Community 5 Other

Documentation and Help

• FAQ (Frequently Asked Questions)

• Cygwin: if you want to use Yices under Windows, you may want to install Cygwin. Here's some help on doing that, from the SAL Wiki

• However, since version 1.0.5, Yices can now be used on Windows without Cygwin. Just download the mingw32 version at the Yices download page

News and Plans

The standard version of Yices that we distribute and maintain is Yices1, first released in 2007. It is still a highly competitive SMT solver. We also distribute and maintain the prototype of Yices2 that participated in the 2009 SMT Competition. It outperforms Yices1 but is not completely compatible with it. We plan to distribute the finished version of Yices2 in 2011; our current work is developing a new architecture and interface for the solver that will make it useful in interactive proof exploration (as in PVS) and not merely as an endgame solver.

SMT Competitions

There is an annual competition for SMT solvers.

2010 

Yices did not enter this year (there was a significant change in the SMT-LIB language and we did not have the resources to develop a new front-end). However, last year's version was automatically entered in the divisions that it won. It continued to win three of them and was runner-up in the other four: http://www.smtexec.org/exec/?jobs=684

2009 

Yices2 prototype won 7 of the 12 divisions it entered and was runner-up in 3: http://www.smtexec.org/exec/?jobs=529

2008 

Yices2 prototype won 2 of the 4 divisions it entered, and was runner-up in a third: http://www.smtexec.org/exec/?jobs=311

2007 

Yices won 6 of the 12 categories and came second in 3: http://www.smtexec.org/exec/?jobs=20

2006

Yices won every division: http://www.smtcomp.org/2006/results.shtml

Community

• Links to papers relevant to Yices
• Links to groups using Yices
• Work on Yices at Pace University, NY, USA
  • Yices Web Interface
  • Yices Java API Lite
  • Yices-Rainbow Eclipse Plugin
• Links to other tools that use Yices
  • CREST: automatic test generation tool for C
  • Kind-A Safety Property Verifier for Lustre Programs
  • MCMT: Model Checker Modulo Theories
• Programming interfaces (other than C API provided with Yices)
  • Haskell - there are multiple ones on Hackage such as
    • yices via IPC through pipe, and
    • yices-easy via C API binding
    • yices-painless via C API binding

Other

We're still learning how best to organize and use this capability--please join in and help.