MMC: the Mono Model Checker

T.C. Ruys, Niels H.M. Aan de Brugh

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    3 Citations (Scopus)

    Abstract

    The Mono Model Checker (MMC) is a software model checker for CIL bytecode programs. MMC has been developed on the Mono platform. MMC is able to detect deadlocks and assertion violations in CIL programs. The design of MMC is inspired by the Java PathFinder (JPF), a model checker for Java programs. The performance of MMC is comparable to JPF. This paper introduces MMC and presents its main architectural characteristics.
    Original languageUndefined
    Title of host publicationProceedings of the Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2007)
    EditorsMarieke Huisman, F. Spoto
    Place of PublicationAmsterdam
    PublisherElsevier
    Pages149-160
    Number of pages12
    DOIs
    Publication statusPublished - 31 Jul 2007

    Publication series

    NameElectronic Notes in Theoretical Computer Science
    PublisherElsevier
    Number1
    Volume190
    ISSN (Print)1571-0661
    ISSN (Electronic)1571-0661

    Keywords

    • EWI-14857
    • METIS-255108
    • IR-65288
    • FMT-MC: MODEL CHECKING

    Cite this

    Ruys, T. C., & Aan de Brugh, N. H. M. (2007). MMC: the Mono Model Checker. In M. Huisman, & F. Spoto (Eds.), Proceedings of the Second Workshop on Bytecode Semantics, Verification, Analysis and Transformation (Bytecode 2007) (pp. 149-160). (Electronic Notes in Theoretical Computer Science; Vol. 190, No. 1). Amsterdam: Elsevier. https://doi.org/10.1016/j.entcs.2007.02.066