We have implemented a series of versions for BACH. Currently, we are working on a brand new version of BACH which supports modeling, falsification, and verification of hybrid systems. It will be relased soon.

Download BACH 5.5 (C++, Newest version, Based on interaction-oriented shallow synchronization semantics)

Download BACH 5.2 (C++, Mixed semantics guided layered BMC)

Download BACH 5.0, (C++, SAT-LP layered BMC plus unbounded proof under certain condition)

Download BACH2.1 (JAVA, DFS+lightweight LP, without IIS)

Download BACH Online

BACH (Eclipse Plug-in)

BACH-SAT (for single LHA, SAT+heavyweight LP, with IIS, require IBM CPLEX to be installed)

BACH-DFS (for single LHA, DFS+heavyweight LP, with IIS, require IBM CPLEX to be installed)

BACH 4.0 (for single LHA, a special editon with bidirectional DFS, with IIS, require IBM CPLEX to be installed)

BACH 3.0, Checker with new underlying LP Solver

BACH 2.0, Compositional checker with old GUI

BACH 1.0, Checker for single LHA

BACH EP, Eclipse plugin version of BACH 1.0

Path-oriented checker for compositional LHA systems.

Path-oriented checker for single LHA.

If you want to download the old versions, please contact the author Lei Bu.