Pipeline Example

This next example will demonstrate how to create a new session, how to specify a property to be checked, and how to use abstractions to extract a smaller model out of the program to be model checked.

• The structure of the Pipeline example
• Writing a specification using the Bandera Specification Language
• Entering a specification using the Bandera User Interface
• Using a simple data abstraction