From: "David L. Rager"
Subject: This Week in ACL2: Finite Models of Theories in Equational Logic
Date: Mon, 17 Jul 2006 18:21:52 -0500

Hello ACL2 Meeting Attendees,

Fadi Zaraket will speak this Wednesday (07/19) on "finite models of theories
in equational logic."  This meeting will occur in ACES 3.116 at 4pm and last
until approximately 5:45pm.  The abstract is below:

We present SERA, a novel algorithm for compiling a class of finitized
relational logic formulas into sequential circuits.

The compiled sequential structures use much fewer variables than traditional
approaches that compile to SAT, and allow us to iteratively apply powerful
reduction, abstraction, and decision algorithms from transformation-based
verification (TBV). Our SERA prototype leverages TBV to analyze formulas
written in Alloy, a first-order language with transitive closure that is
based on relations. The experimental results show that SERA can check
formulas for scopes-bounds on universe of discourse-that are an order of
magnitude higher than those feasible with existing combinational approaches
such as the Alloy Analyzer.

Hope to see you there,
David