Effective Bug Hunting with SPIN and Modex

Gerard J. Holzmann, Theo C. Ruys

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    9 Citations (Scopus)
    206 Downloads (Pure)


    This tutorial consists of two parts. In the first part we present an advanced overview of SPIN, and illustrate its practical application to logic model checking problems. In the second part of the tutorial we present an overview of a related tool called Modex. Modex can be used to extract Spin verification models directly from C source code. It supports the definition of user-defined abstractions, and cleverly exploits the capability in Spin version 4 to include embedded C code inside abstract verification models. We will show how to use Spin and Modex, separately and combined, in an effective way when searching for design errors in distributed software applications. Both Spin and Modex are written in ANSI-C and can freely be used on research projects.
    Original languageEnglish
    Title of host publicationModel Checking Software
    Subtitle of host publication12th International SPIN Workshop, San Francisco, CA, USA, August 22-24, 2005, Proceedings
    Place of PublicationBerlin, Heidelberg
    Number of pages1
    ISBN (Electronic)978-3-540-31899-6
    ISBN (Print)978-3-540-28195-5
    Publication statusPublished - Aug 2005
    Event12th International SPIN Workshop on Model Checking Software 2005 - San Francisco, United States
    Duration: 22 Aug 200524 Aug 2005
    Conference number: 12

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743


    Workshop12th International SPIN Workshop on Model Checking Software 2005
    Country/TerritoryUnited States
    CitySan Francisco




    Dive into the research topics of 'Effective Bug Hunting with SPIN and Modex'. Together they form a unique fingerprint.

    Cite this