Building your own software model checker using the Bogor extensible model checking framework Model checking has proven to be an effective technology for verification and debugging in hardware and more recently in software domains. We believe that recent trends in both the requirements for software systems and the processes by which systems are developed suggest that domain-specific model checking engines may be more effective than general purpose model checking tools. To overcome limitations of existing tools which tend to be monolithic and non-extensible, we have developed an extensible and customizable model checking framework called Bogor. In this tool paper, we summarize (a) Bogor’s direct support for modeling object-oriented designs and implementations, (b) its facilities for extending and customizing its modeling language and algorithms to create domain-specific model checking engines, and (c) pedagogical materials that we have developed to describe the construction of model checking tools built on top of the Bogor infrastructure

References in zbMATH (referenced in 36 articles )

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

1 2 next

  1. Groce, Alex; Havelund, Klaus; Holzmann, Gerard; Joshi, Rajeev; Xu, Ru-Gang: Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (2014)
  2. Beckert, Bernhard; Klebanov, Vladimir: A dynamic logic for deductive verification of multi-threaded programs (2013)
  3. Rafe, Vahid; Nikanjam, Amin; Rezaei, Mohammad: Galoan: A multi-agent approach to herd cows (2011)
  4. Siegel, Stephen F.; Zirkel, Timothy K.: TASS: the toolkit for accurate scientific software (2011)
  5. Weber, Michael: An embeddable virtual machine for state space generation (2010)
  6. Yang, Yu; Chen, Xiaofang; Gopalakrishnan, Ganesh; Kirby, Robert M.: Distributed dynamic partial order reduction (2010)
  7. Zambon, Eduardo: Using graph transformations and graph abstractions for software verification (2010)
  8. del Mar Gallardo, María; Merino, Pedro; Sanán, David: Model checking dynamic memory allocation in operating systems (2009)
  9. Rafe, Vahid; Rahmani, Adel T.: Towards automated software model checking using graph transformation systems and bogor (2009)
  10. Baresi, Luciano; Rafe, Vahid; Rahmani, Adel T.; Spoletini, Paola: An efficient solution for model checking graph transformation systems (2008)
  11. Deloach, Scott A.; Oyenan, Walamitien H.; Matson, Eric T.: A capabilities-based model for adaptive organizations. (2008)
  12. Ghezzi, Carlo; Inverardi, Paola; Montangero, Carlo: Dynamically evolvable dependable software: From oxymoron to reality (2008)
  13. Ivančić, Franjo; Yang, Zijiang; Ganai, Malay K.; Gupta, Aarti; Ashar, Pranav: Efficient SAT-based bounded model checking for software verification (2008)
  14. Rafe, Vahid; Rahmani, Adel T.: Formal analysis of workflows using UML 2.0 activities and graph transformation systems (2008)
  15. Rafe, Vahid; Rahmani, Adel T.: A graph transformation-based approach to formal modeling and verification of workflows (2008)
  16. Matousek, Tomas; Zavoral, Filip: Extracting Zing models from C source code (2007)
  17. Bordini, Rafael H.; Fisher, Michael; Visser, Willem; Wooldridge, Michael: Verifying multi-agent programs by model checking. (2006)
  18. Ghica, D.R.; Murawski, A.S.: Compositional model extraction for higher-order concurrent programs (2006)
  19. Robby; Rodríguez, Edwin; Dwyer, Matthew B.; Hatcliff, John: Checking JML specifications using an extensible software model checking framework (2006)
  20. Zhang, Hongyu; Bradbury, Jeremy S.; Cordy, James R.; Dingel, Juergen: Using source transformation to test and model check implicit-invocation systems (2006)

1 2 next