- 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
- Inez is a constraint solver that implements the ILP Modulo Theories (IMT) scheme, as described in our CAV 2013 paper. 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 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. These examples and many more are included.
- 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 recent improvements to termination analysis, etc.
- 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.