About BEG

Bandera Environment Generator (BEG) supports automated environment generation to provide a restricted form of modular model checking of Java programs. Specifically, we consider decomposition of a Java program into two parts: a unit under analysis (or unit) and its environment. A unit is any collection of Java classes and its environment consists of the classes with which the unit interacts through the unit's interface. The unit's source code is the subject of verification along with an abstract model of the environments externally observable behavior. The environment model is derived from specifications written by the user or from the results of analyzing source code that implements environment components. Existing abstraction techniques may be applied to local unit data and to the data that flows between the unit and environment. The resulting abstracted unit and environment may then be analyzed against the unit properties by existing Java model checking frameworks such as Bandera and Java PathFinder (JPF).