The goal of the Bandera project is to integrate existing programming language processing techniques with newly developed techniques to provide automated support for the extraction of safe, compact, finite-state models that are suitable for verification from Java source code. While our ultimate goal is fully-automated model extraction for a broad class of software systems, our approach takes as a given that guidance from a software analyst may be requied.
Bandera directory