Erik Reeber, 11/28/07

Email message:

Hello,

    At this week's ACL2 seminar, I will be talking about my SULFA tool, 
which is available with the standard ACL2 distribution.  The tool verifies 
a certain subclass of ACL2 formulas automatically (the Subclass of 
Unrollable List Formulas) and generates counterexamples to invalid SULFA 
formulas.

    In the talk, I will start with some basic examples showing how to 
verify formulas from propositional logic and then add list data 
structures.  I will then show how to get the tool to play Sudoku, before 
going into some more serious examples from hardware verification.  I will 
also talk about how to track down bugs using the generated counterexamples 
and discuss the construction of ACL2 models in a way that leads to 
efficient SULFA formulas.

    I hope to see you all there.

Thanks,
Erik