Softwares & Tools


EB2ALL is set of plugins for Rodin and the translation of Event-B models into C,C++,Java codes Consult the web page


TLAPS, the TLA+ proof system The TLA+ Proof System (TLAPS) is a platform for computerized verification of TLA+ proofs using formal reasoning systems such as automated theorem provers, proof-assistants, SMT/SAT solvers, and decision procedures. The TLA+ proof language is declarative, hierarchical, and scalable to large system specifications. It provides a consistent abstraction over the various "backend" verifiers. TLAPS is free software, distributed under a BSD-like license. Consult the web page


veriT is a SMT (Satisfiability Modulo Theories) solver Consult the web page