Related Projects

  • We actively collaborate with NASA Ames's Automated Software Engineering Lab on a variety of issues related to software model-checking. The NASA Ames model-checker Java PathFinder is one of the backend model-checkers supported by Bandera.
  • We also actively collaborate with researchers from the University of Massachusetts on the SCARP project.
  • The BLAST lazy abstraction software verification tool for C programs from University of Berkeley.
  • The SLAM Project at Microsoft Research for model-checking C programs from Microsoft Research.
  • The TVLA Project using three-valued logic for static analysis at the University of Tel-Aviv.
  • The CANVAS Project on component verification from IBM and the University of Tel-Aviv.
  • FeaVer (Feature Verification System) is a standalone tool for verification of general software written in ANSI-C from Bell Labs.
  • Bandera uses the Soot Java compiler infrastructure from the Sable Group at the University of McGill.
  • Bandera incorporates the Spin (Bell Labs), dSpin (Kansas State), and HSF-Spin (University of Freiborg) model-checkers.
  • Bandera makes use of the OpenJGraph graphing library and the GEF graphing library in the implementation of the counter example GUI and can be extended to use Grappa and the JGraph graphing library.
  • Bandera has incorporated the code from the open source project JWF to implement the session file wizard.