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