News
- BAT: The Bit-level Analysis Tool has been updated.
BAT has been made more efficient, and we are now releasing source code!
- I created a new Web page describing our
CoBaSA work on the synthesis of system architectures. CoBaSa
was used to synthesize system architectures for Boeing's
Dreamliner from high-level constraints that included resource,
communication, and real-time constraints.
-
Inez, our IMT (ILP Modulo Theories) solver is now available on Github.
- The ACL2 books are now available in paperback form from
the just-in-time online publisher lulu.
- 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.
- Looking for a bit-vector reasoning tool? Consider using 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 considering using a Bloom filter? Use my
Bloom
filter calculator to compute the optimal settings,
determine false positive rates, and much more.
Upcoming conferences and events