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 134 articles )

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

1 2 3 ... 5 6 7 next

  1. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  2. Shankar, Natarajan: Combining model checking and deduction (2018)
  3. Jančík, Pavel; Kofroň, Jan: On partial state matching (2017)
  4. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  5. Prabhakar, Pavithra; Duggirala, Parasara Sridhar; Mitra, Sayan; Viswanathan, Mahesh: Hybrid automata-based CEGAR for rectangular hybrid systems (2015)
  6. Thomsen, Bent; Luckow, Kasper Søe; Leth, Lone; Bøgholm, Thomas: From safety critical Java programs to timed process models (2015)
  7. Groce, Alex; Havelund, Klaus; Holzmann, Gerard; Joshi, Rajeev; Xu, Ru-Gang: Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (2014)
  8. Perna, Juan I.; George, Chris: Model checking RAISE applicative specifications (2013)
  9. Gallardo, M. M.; Joubert, C.; Merino, P.; Sanán, D.: A model-extraction approach to verifying concurrent C programs with CADP (2012) ioport
  10. Ribeiro, Leila; Dos Santos, Osmar Marchi; Dotti, Fernando Luís; Foss, Luciana: Correct transformation: from object-based graph grammars to PROMELA (2012)
  11. Schlich, Bastian; Brauer, Jörg; Kowalewski, Stefan: Application of static analyses for state-space reduction to the microcontroller binary code (2011)
  12. Siegel, Stephen F.; Zirkel, Timothy K.: TASS: the toolkit for accurate scientific software (2011)
  13. 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)
  14. Artho, Cyrille; Hagiya, Masami; Leungwattanakit, Watcharin; Tanabe, Yoshinori; Yamamoto, Mitsuharu: Model checking of concurrent algorithms: from Java to C (2010)
  15. Bošnački, Dragan; Edelkamp, Stefan: Model checking software: on some new waves and some evergreens (2010) ioport
  16. Goldman, Max; Katz, Emilia; Katz, Shmuel: MAVEN: Modular aspect verification and interference analysis (2010)
  17. Grinchtein, Olga; Jonsson, Bengt; Leucker, Martin: Learning of event-recording automata (2010)
  18. Plagge, Daniel; Leuschel, Michael: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more (2010) ioport
  19. Abed, Sa’ed; Mohamed, Otmane Ait: LCF-style platform based on multiway decision graphs (2009)
  20. del Mar Gallardo, María; Merino, Pedro; Sanán, David: Model checking dynamic memory allocation in operating systems (2009)

1 2 3 ... 5 6 7 next

Further publications can be found at: