This section illustrates the basic features of Bandera with some simple examples included in the distribution. First, we'll start by running some sessions that have already been defined. This will illustrate the code browser, slicing, and counterexample displays. Next, we'll step through the process of creating several new sessions. This will illustrate the process of using the property specification tool (Property Manager) and the abstraction component. The remaining sections of the tutorial will explain the components illustrated here in greater detail.
Before you can step through the examples below, the Spin
model checker must be installed, and you'll need to
copy the tutorial directory included with Bandera
into your own directory hierarchy.
