dSPIN is an extension of the SPIN model checker that offers efficient means for the verification of concurrent programs written in high(er)-level programming languages. It provides a number of novel features implemented on top of standard SPIN’s state space exploration and reduction algorithms: memory references (pointers); dynamic memory allocation/deletion; recursive functions; function code references (function pointers); garbage collection; symmetry reductions. The design of dSPIN is driven by the need to enhance the expressiveness of existing modeling techniques, while coping with potential complexity blow-ups caused by adding extra functionalities. The input language of dSPIN is a superset of PROMELA containing a small number of new constructs such as pointer type variables, memory allocation statements, function definitions and invocations. Such constructs are supported by both the random simulator and verifier generator. The tool is SPIN-backwards compatible that is, every standard SPIN model can be also verified using dSPIN instead.

References in zbMATH (referenced in 32 articles )

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

1 2 next

  1. De Nicola, Rocco; Lluch Lafuente, Alberto; Loreti, Michele; Morichetta, Andrea; Pugliese, Rosario; Senni, Valerio; Tiezzi, Francesco: Programming and verifying component ensembles (2014)
  2. del Mar Gallardo, María; Merino, Pedro; Sanán, David: Model checking dynamic memory allocation in operating systems (2009)
  3. Trofin, Mircea; Murphy, John: Static verification of component composition in contextual composition frameworks (2008)
  4. Grumberg, Orna; Katz, Shmuel: VeriTech: a framework for translating among model description notations (2007)
  5. Clarke, Dave: Reasoning about connector reconfiguration II: Basic reconfiguration logic. (2006)
  6. Dotti, Fernando Luís; Ribeiro, Leila; Dos Santos, Osmar Marchi; Pasini, Fábio: Verifying object-based graph grammars (2006)
  7. Madl, Gabor; Abdelwahed, Sherif; Schmidt, Douglas C.: Verifying distributed real-time properties of embedded systems via graph transformations and model checking (2006)
  8. Palmer, Robert; Barrus, Steve; Yang, Yu; Gopalakrishnan, Ganesh; Kirby, Robert M.: Gauss: A framework for verifying scientific computing software. (2006)
  9. Iosif, Radu; Dwyer, Matthew B.; Hatcliff, John: Translating Java for multiple model checkers: The Bandera back-end (2005)
  10. Kumar, Rahul; Mercer, Eric G.: Load balancing parallel explicit state model checking. (2005)
  11. Kumar, Rahul; Mercer, Eric G.: Load balancing parallel explicit state model checking (2005)
  12. Lakos, Charles A.; Kristensen, Lars M.: State space exploration of object-based systems using equivalence reduction and the sweepline method (2005)
  13. Penix, John; Visser, Willem; Park, SeungJoon; Pasareanu, Corina; Engstrom, Eric; Larson, Aaron; Weininger, Nicholas: Verifying time partitioning in the DEOS scheduling kernel (2005)
  14. Andrews, Tony; Qadeer, Shaz; Rajamani, Sriram K.; Rehof, Jakob; Xie, Yichen: Zing: A model checker for concurrent software (2004)
  15. Dwyer, Matthew; Leue, Stefan: Introductory paper (2004)
  16. Dwyer, Matthew; Leue, Stefan: Introductory paper (2004)
  17. Gardner, Philippa (ed.); Yoshida, Nobuko (ed.): CONCUR 2004 -- concurrency theory. 15th international conference, London, UK, August 31 -- September 3, 2004. Proceedings. (2004)
  18. Groce, Alex; Visser, Willem: Heuristics for model checking Java programs (2004)
  19. Groce, Alex; Visser, Willem: Heuristics for model checking Java programs (2004)
  20. Iosif, Radu: Symmetry reductions for model checking of concurrent dynamic software (2004)

1 2 next