Runs of Bandera are configured using sessions. A session is a record holding information about the file name(s) of the source code to be checked during the run, the property to be checked, the tool components that are to be enabled during the run, options and settings for the selected components, the particular back-end model-checker to be used, and other miscellaneous information such as location of working directories into which temporary output should be dumped.
Multiple session records are held in a session file. When performing a new run of Bandera, the session record can be saved in a session file and loaded at a later time. This allows the user to avoid restating all option information, etc. Session records in a session file can also be processed in batch mode using a command line flag. This is useful for performing regression tests on software under development. For example, you might consider creating a session file holding all the checks that you usually run on a piece of software, then using the batch mode facility to run all of the model-checks specified in the session file overnight.
The upper-left toolbar buttons are used for manipulating session files such as New, Open, Save As, and Save.