A Comparison of Modular Verification Techniques

Henrik Reif Andersen; Jørgen Staunstrup; Niels Maretti

A Comparison of Modular Verification Techniques

Henrik Reif Andersen
, Jørgen Staunstrup
, Niels Maretti

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 language	English
Title of host publication	Proceedings of TAPSOFT'97, LNCS 1214
Place of Publication	Berlin, Heidelberg
Publisher	Springer Verlag
Publication date	1997
Pages	550-564
Publication status	Published - 1997
Event	7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development - Lille, France Duration: 14 Apr 1997 → 18 Apr 1997

Conference

Conference	7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development
Country/Territory	France
City	Lille
Period	14/04/1997 → 18/04/1997

OpenUrl availability

Check availability in DTU Findit

Cite this

@inproceedings{3e41bb0c70414452a34cf79db826c89c,

title = "A Comparison of Modular Verification Techniques",

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.",

author = "Andersen, \{Henrik Reif\} and J{\o}rgen Staunstrup and Niels Maretti",

year = "1997",

language = "English",

pages = "550--564",

booktitle = "Proceedings of TAPSOFT'97, LNCS 1214",

publisher = "Springer Verlag",

address = "Germany",

note = "7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development , TAPSOFT'97 ; Conference date: 14-04-1997 Through 18-04-1997",

}

TY - GEN

T1 - A Comparison of Modular Verification Techniques

AU - Andersen, Henrik Reif

AU - Staunstrup, Jørgen

AU - Maretti, Niels

PY - 1997

Y1 - 1997

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

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

M3 - Article in proceedings

SP - 550

EP - 564

BT - Proceedings of TAPSOFT'97, LNCS 1214

PB - Springer Verlag

CY - Berlin, Heidelberg

T2 - 7th International Joint Conference CAAP/FASE on Theory and Practice of Software Development

Y2 - 14 April 1997 through 18 April 1997

ER -