- ACL2s: The
ACL2 Sedan: ACL2s is a powerful theorem proving system based
on the ACL2
theorem prover. Our goal is to bring formal reasoning to
the masses. To that end, ACL2s features enchancements such as a
modern graphical integrated development environment in Eclipse,
levels appropriate for beginners through experts,
state-of-the-art enhancements such as our CCG termination
analysis, counterexample generation, a data definition framework
with support for polymorphic types, etc. We have used ACL2s to
teach thousands of undergraduate students at Northeastern
University (and several other universities) how to reason about
computation.
- CoBaSA is a framework for
synthesizing systems. It was used to successfully synthesize system
architectures for Boeing's 787 (Dreamliner) and it was designed to be
generally applicable.
- Inez is
the latest version of CoBaSA. It is a
constraint solver that implements the ILP Modulo Theories (IMT)
scheme, as described in our CAV 2013 paper. It An IMT instance
is an Integer Linear Programming instance, where some symbols
have interpretations in background theories. We have used the
IMT approach to solve industrial synthesis and design problems
with real-time constraints arising in the development of the
Boeing 787. Inez can be used to solve problems involving linear
constraints and optimization. Inez is OCaml-centric. The
preferred mode of interacting with the solver is via scripts
written in a Camlp4-powered superset of OCaml.
- BAT: The Bit-level Analysis Tool:
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 was first released in 2006, and can be
thought of as an SMT solver for the extensional theory of arrays
and bit-vectors. BAT is an eager solver that uses
term-rewriting as a preprocessing step and then generates SAT
instances. BAT has been used to solve problems that cannot be
handled by any other decision procedure we have tried (circa
2010). For example, BAT can prove that a 32-bit 5 stage
pipelined machine model refines its ISA in approximately 2
minutes. These examples and many more are included in the
distribution. As of October 2014, we are releasing a more
efficient version of BAT, along with the sources.
- Bloom
filter calculator: The Bloom filter calculator has been
used over 20,000 times by a variety of users. It is a Web
application that can be used to compute optimal
settings, determine false positive rates, and much more.
- 3Spin and X3Spin: Modified versions of the Spin model checker
with advances in the efficiency, configurability, and
usability of probabilistic explicit-state verification.
- 3Murphi: A modified version of the Murphi verifier with
advances in the efficiency, configurability, and usability
of probabilistic explicit-state verification.