Pete's Webpage

News

The ACL2 books are now available in paperback form from the just-in-time online publisher lulu.
- Matt Kaufmann, Panagiotis Manolios, and J Moore. Computer-Aided Reasoning: An Approach.
- Matt Kaufmann, Panagiotis Manolios, and J Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies.
We recently released the BAT: The Bit-level Analysis Tool. BAT is a tool for deciding bounded model checking and k-induction queries for a powerful hardware description language that is strongly typed (with type inference), includes bit vectors, memories, and the standard operations on these data types, allows for user defined functions, functions which return multiple values, etc. BAT has been used to solve problems that cannot be handled by any other decision procedure we have tried. For example, BAT can prove that a 32-bit 5 stage pipelined machine model refines its ISA in approximately 2 minutes.
Are you a user of ACL2 or interested in learning how to use the theorem prover? Then definitely look at the ACL2s system we are developing. It features a modern graphical integrated development environment in Eclipse, levels appropriate for beginners through experts, state-of-the-art enhancements such as our recent improvements to termination analysis, etc.
Are you considering using a Bloom filter? Use my Bloom filter calculator to compute the optimal settings, determine false positive rates, and much more.