Below you will find the PowerPoint slides for talks that we have given recently. Many of the talks give overviews of Bandera to slightly different audiences -- thus, several are quite similar. The most recent overview is John Hatcliff's lecture on Bandera at SFM'02. If you are interested in using Bandera in a course, you might take a look at the slides by Matt Dwyer, John Hatcliff, and Willem Visser from a six-hour tutorial at ETAPS 2002.
- John Hatcliff's slides from the International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM '02) in Bertinoro, Italy. September 9-14, 2002: Lecture 1 (Bandera), Lecture 2 (Specification Patterns), Lecture 3 (Cadena).
- PDF and PowerPoint slidesfrom a six-hour tutorial given at ETAPS 2002 (.zip file)
- John Hatcliff's invited talk from the post-CAV workshop on software model-checking (SMC'01). This talk gives a gentle overview of Bandera and is targetted at an audience who is familiar with model-checking but not necessarily issues related to software model-checking.
- Corina Pasareanu's ICSE'01 talk about Bandera's abstraction facilities and JPF model-checking as applied to the scheduler from the DEOS real-time operating system.
- Corina Pasareanu's TACAS'01 talk modifying the JPF model-checking to produce feasible counter-examples.
- John Hatcliff gave a series of talks as part of a BRICS mini-course in Aarhus, Denmark in Oct. 2000 that give a Bandera overview, a demo of the Bandera toolset, a description of temporal specification, a survey of how such specifications are supported in the Bandera Specification Language, and how slicing in Bandera works. If you are considering using Bandera in a course you are teaching, you might find these talks helpful.
- John Hatcliff's ICSE'2000 Bandera talk and Matt Dwyer's extended version of the talk (with screen shots of the Bandera GUI) given at the VIRES workshop, June, 2000.