Using the Bandera tool set to model-check properties of concurrent Java software The Bandera Tool Set is an integrated collection of program analysis, transformation, and visualization components designed to facilitate experimentation with model-checking Java source code. Bandera takes as input Java source code and a software requirement formalized in Bandera’s temporal specification language, and it generates a program model and specification in the input language of one of several existing model-checking tools (including Spin, dSpin, SMV, and JPF). Both program slicing and user extensible abstract interpretation components are applied to customize the program model to the property being checked. When a model-checker produces an error trail, Bandera renders the error trail at the source code level and allows the user to step through the code along the path of the trail while displaying values of variables and internal states of Java lock objects. par In this tutorial paper, we use a simple concurrent Java program to illustrate the functionality of the main components of Bandera and how to interact the tool set using its graphical user interface.

References in zbMATH (referenced in 149 articles )

Showing results 1 to 20 of 149.
Sorted by year (citations)

1 2 3 ... 6 7 8 next

  1. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2015)
  2. Groce, Alex; Havelund, Klaus; Holzmann, Gerard; Joshi, Rajeev; Xu, Ru-Gang: Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (2014)
  3. Perna, Juan I.; George, Chris: Model checking RAISE applicative specifications (2013)
  4. Gallardo, M.M.; Joubert, C.; Merino, P.; Sanán, D.: A model-extraction approach to verifying concurrent C programs with CADP (2012)
  5. Ribeiro, Leila; Dos Santos, Osmar Marchi; Dotti, Fernando Luís; Foss, Luciana: Correct transformation: from object-based graph grammars to PROMELA (2012)
  6. Schlich, Bastian; Brauer, Jörg; Kowalewski, Stefan: Application of static analyses for state-space reduction to the microcontroller binary code (2011)
  7. Siegel, Stephen F.; Zirkel, Timothy K.: TASS: the toolkit for accurate scientific software (2011)
  8. van Gastel, Bernard; Lensink, Leonard; Smetsers, Sjaak; van Eekelen, Marko: Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving (2011)
  9. Bošnački, Dragan; Edelkamp, Stefan: Model checking software: on some new waves and some evergreens (2010)
  10. Goldman, Max; Katz, Emilia; Katz, Shmuel: MAVEN: Modular aspect verification and interference analysis (2010)
  11. Grinchtein, Olga; Jonsson, Bengt; Leucker, Martin: Learning of event-recording automata (2010)
  12. Plagge, Daniel; Leuschel, Michael: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more (2010)
  13. Abed, Sa’ed; Mohamed, Otmane Ait: LCF-style platform based on multiway decision graphs (2009)
  14. Abed, Sa’ed; Mohamed, Otmane Aït: LCF-style platform based on multiway decision graphs (2009)
  15. del Mar Gallardo, María; Merino, Pedro; Sanán, David: Model checking dynamic memory allocation in operating systems (2009)
  16. Güleşir, Gürcan; van den Berg, Klaas; Bergmans, Lodewijk; Akşit, Mehmet: Experimental evaluation of a tool for the verification and transformation of source code in event-driven systems (2009)
  17. Lochbihler, Andreas; Snelting, Gregor: On temporal path conditions in dependence graphs (2009)
  18. Matousek, Tomas; Jezek, Pavel: Despec: modeling the windows driver environment (2009)
  19. Xu, Dian-Xiang; El-Ariss, Omar; Xu, Wei-Feng; Wang, Lin-Zhang: Aspect-oriented modeling and verification with finite state machines (2009)
  20. Alba, Enrique; Chicano, Francisco: Observations in using parallel and sequential evolutionary algorithms for automatic software testing (2008)

1 2 3 ... 6 7 8 next

Further publications can be found at: