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

Showing results 1 to 20 of 31.
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) ioport
  4. Grumberg, Orna; Katz, Shmuel: VeriTech: a framework for translating among model description notations (2007) ioport
  5. Veanes, Margus; Ernits, Juhan; Campbell, Colin: State isomorphism in model programs with abstract data structures (2007)
  6. Dotti, Fernando Luís; Ribeiro, Leila; Dos Santos, Osmar Marchi; Pasini, Fábio: Verifying object-based graph grammars (2006) ioport
  7. Madl, Gabor; Abdelwahed, Sherif; Schmidt, Douglas C.: Verifying distributed real-time properties of embedded systems via graph transformations and model checking (2006)
  8. Iosif, Radu; Dwyer, Matthew B.; Hatcliff, John: Translating Java for multiple model checkers: The Bandera back-end (2005)
  9. Kumar, Rahul; Mercer, Eric G.: Load balancing parallel explicit state model checking (2005)
  10. Lakos, Charles A.; Kristensen, Lars M.: State space exploration of object-based systems using equivalence reduction and the sweepline method (2005)
  11. Penix, John; Visser, Willem; Park, SeungJoon; Pasareanu, Corina; Engstrom, Eric; Larson, Aaron; Weininger, Nicholas: Verifying time partitioning in the DEOS scheduling kernel (2005)
  12. Andrews, Tony; Qadeer, Shaz; Rajamani, Sriram K.; Rehof, Jakob; Xie, Yichen: Zing: A model checker for concurrent software (2004)
  13. Dwyer, Matthew; Leue, Stefan: Introductory paper (2004) ioport
  14. Dwyer, Matthew; Leue, Stefan: Introductory paper (2004) ioport
  15. Gardner, Philippa (ed.); Yoshida, Nobuko (ed.): CONCUR 2004 -- concurrency theory. 15th international conference, London, UK, August 31 -- September 3, 2004. Proceedings. (2004)
  16. Groce, Alex; Visser, Willem: Heuristics for model checking Java programs (2004) ioport
  17. Groce, Alex; Visser, Willem: Heuristics for model checking Java programs (2004) ioport
  18. Iosif, Radu: Symmetry reductions for model checking of concurrent dynamic software (2004) ioport
  19. Iosif, Radu: Symmetry reductions for model checking of concurrent dynamic software (2004) ioport
  20. Leven, Peter; Mehler, Tilman; Edelkamp, Stefan: Directed error detection in C++ with the assembly-level model checker StEAM (2004)

1 2 next