Date: Tue, 5 Sep 2006 12:24:56 -0500 (CDT)
From: Erik H. Reeber

Hello everyone,

    At this week's ACL2 meeting, after an extended roundtable, I'm going to 
give a short talk on yices.  Yices is an SMT (SAT Modulo Theory) solver 
developed at SRI.  It includes techniques for automatically verifying 
first-order properties involving arithmetic, quantifiers, propositional 
logic, and uninterpreted functions.  It uses a general typing mechanism 
which includes recursive data-types, built on top of booleans, bit 
vectors, integers, and real numbers.

    I'm going to show off how we can use the recursive data-type mechanism 
to implement lists and trees.  Also, I'll use the arithmetic decision 
procedure to prove some examples of arithmetic theorems that I had 
trouble proving in ACL2.  Finally I've translated one of the benchmark 
problems from my SAT paper into yices, and I'll show the results---my SAT 
procedure appears to exhibit considerably better performance than yices 
on this benchmark problem.

-Erik