dSPIN: a model checker for programs


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: 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.


Related papers



Please send any kind of feedback to: Radu.Iosif#imag.fr (where # is @)

Last updated Apr 13 2001 by Radu Iosif