Using BEG

This page is meant for santos people. We are working on including the BEG into Bandera tools and making it available for others.

There are two problems the tools addresses:

1. Generation of the missing environment: given a unit (and no environment), the tool generates the environment for it. There are two types of the environments the tool can generate:

2. Generation of the compact representation of the given envirnoment: given a unit and the implementation of the environment, the tool performs a static analysis of the environment and generates a safe compact representation for the environment classes according to the static analysis information.

Where to find it

I've installed

How to run it