The BRAIN homepage

This page (as well as the BRAIN itself) is in it's preliminary stage of development. We hope to make both of them better soon.

BRAIN stands for Backward Reachability Analysis with INtegers. As an acronym, it should probably be called BRAIN, but we prefer to call it the BRAIN. The BRAIN is an infinite-state model checker which can verify reachability properties, including deadlock-detection. A state for the BRAIN is a finite vector of integers. If reachability is detected, the BRAIN also shows a trace of vectors leading from an initial state to a final (or to a deadlock) state, together with the transitions applied to obtain this trace.

There are two papers related to the BRAIN, both are currently submitted.

1. Using canonical representations of solutions to speed up infinite-state model checking. This paper explain the algorithms used in the BRAIN.
2. A logical reconstruction of reachability. This paper discussed symbolic reachability analysis formalisation and algorithms.

The BRAIN has a simple syntax. The easiest way to learn the syntax is by checking this specification of the barber protocol. Consider this specification as a BRAIN mini-tutorial. More example can be found in examples.zip. Most of these examples are taken from Giorgio Delzanno's homepage. We do not claim that these examples are correct representations of industrial-quality protocols, but believe that many of them are. If you want to check deadlock-freedom, simply type 'deadlock' instead of a specification of final states.

Two executables of the BRAIN are available:

1. brain-linux.gz for Linux-based PCs.
2. brain-solaris.gz for SPARC running Solaris.

These versions are slightly improved compared to those described in the paper. For example, they may consume up to 8 times less memory on hard examples.