A Comparison of Modular Verification Techniques

Henrik Reif Andersen, Jørgen Staunstrup, Niels Maretti

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    This paper presents and compares three techniques for mechanized verification of state oriented design descriptions. One is a traditional forwardgeneration of a fixed point characterizing the reachable states. The two others can utilize a modular structure provided by the designer. Onerequires a substantial manual effort by the designer, but is computationally very efficient, while the other requires almost no manual assistance with a much better performance than the simple forward generation. The performance of the three techniques is compared on a set of examples.
    Original languageEnglish
    Title of host publicationProceedings of TAPSOFT'97, LNCS 1214
    Place of PublicationBerlin, Heidelberg
    PublisherSpringer Verlag
    Publication date1997
    Pages550-564
    Publication statusPublished - 1997
    EventTAPSOFT'97, Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE - Lille, France
    Duration: 1 Jan 1997 → …

    Conference

    ConferenceTAPSOFT'97, Theory and Practice of Software Development, 7th International Joint Conference CAAP/FASE
    CityLille, France
    Period01/01/1997 → …

    Cite this

    Andersen, H. R., Staunstrup, J., & Maretti, N. (1997). A Comparison of Modular Verification Techniques. In Proceedings of TAPSOFT'97, LNCS 1214 (pp. 550-564). Springer Verlag.