The fixpoint-analysis machine

Bernhard Steffen; Andreas Claßen; Marion Klein; Jens Knoop; Tiziana Margaria

doi:10.1007/3-540-60218-6_6

The fixpoint-analysis machine

Bernhard Steffen, Andreas Claßen, Marion Klein, Jens Knoop, Tiziana Margaria

University of Passau

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

We present a fixpoint-analysis machine, for the efficient computation of homogeneous, hierarchical, and alternating fixpoints over regular, context-free/push-down and macro models. Applications of such fixpoint computations include intra- and interprocedural data flow analysis, model checking for various temporal logics, and the verification of behavioural relations between distributed systems. The fixpoint-analysis machine identifies an adequate (parameterized) level for a uniform treatment of all those problems, which, despite its uniformity, outperforms the ‘standard iteration based’ special purpose tools usually by factors around 10, even if the additional compilation time is taken into account.

Original language	English
Title of host publication	CONCUR 1995
Subtitle of host publication	Concurrency Theory - 6th International Conference, Proceedings
Editors	Insup Lee, Scott A. Smolka
Publisher	Springer Verlag
Pages	72-87
Number of pages	16
ISBN (Print)	3540602186, 9783540602187
DOIs	https://doi.org/10.1007/3-540-60218-6_6
Publication status	Published - 1995
Externally published	Yes
Event	6th International Conference on Concurrency Theory, CONCUR 1995 - Philadelphia, United States Duration: 21 Aug 1995 → 24 Aug 1995

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	962
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	6th International Conference on Concurrency Theory, CONCUR 1995
Country/Territory	United States
City	Philadelphia
Period	21/08/95 → 24/08/95

Access to Document

10.1007/3-540-60218-6_6

Cite this

Steffen, B., Claßen, A., Klein, M., Knoop, J., & Margaria, T. (1995). The fixpoint-analysis machine. In I. Lee, & S. A. Smolka (Eds.), CONCUR 1995: Concurrency Theory - 6th International Conference, Proceedings (pp. 72-87). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 962). Springer Verlag. https://doi.org/10.1007/3-540-60218-6_6

Steffen, Bernhard ; Claßen, Andreas ; Klein, Marion et al. / The fixpoint-analysis machine. CONCUR 1995: Concurrency Theory - 6th International Conference, Proceedings. editor / Insup Lee ; Scott A. Smolka. Springer Verlag, 1995. pp. 72-87 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{709ef014a6d645c382329781f595712c,

title = "The fixpoint-analysis machine",

abstract = "We present a fixpoint-analysis machine, for the efficient computation of homogeneous, hierarchical, and alternating fixpoints over regular, context-free/push-down and macro models. Applications of such fixpoint computations include intra- and interprocedural data flow analysis, model checking for various temporal logics, and the verification of behavioural relations between distributed systems. The fixpoint-analysis machine identifies an adequate (parameterized) level for a uniform treatment of all those problems, which, despite its uniformity, outperforms the {\textquoteleft}standard iteration based{\textquoteright} special purpose tools usually by factors around 10, even if the additional compilation time is taken into account.",

author = "Bernhard Steffen and Andreas Cla{\ss}en and Marion Klein and Jens Knoop and Tiziana Margaria",

note = "Publisher Copyright: {\textcopyright} 1995, Springer Verlag. All rights reserved.; 6th International Conference on Concurrency Theory, CONCUR 1995 ; Conference date: 21-08-1995 Through 24-08-1995",

year = "1995",

doi = "10.1007/3-540-60218-6_6",

language = "English",

isbn = "3540602186",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "72--87",

editor = "Insup Lee and Smolka, {Scott A.}",

booktitle = "CONCUR 1995",

}

Steffen, B, Claßen, A, Klein, M, Knoop, J & Margaria, T 1995, The fixpoint-analysis machine. in I Lee & SA Smolka (eds), CONCUR 1995: Concurrency Theory - 6th International Conference, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 962, Springer Verlag, pp. 72-87, 6th International Conference on Concurrency Theory, CONCUR 1995, Philadelphia, United States, 21/08/95. https://doi.org/10.1007/3-540-60218-6_6

The fixpoint-analysis machine. / Steffen, Bernhard; Claßen, Andreas; Klein, Marion et al.
CONCUR 1995: Concurrency Theory - 6th International Conference, Proceedings. ed. / Insup Lee; Scott A. Smolka. Springer Verlag, 1995. p. 72-87 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 962).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - The fixpoint-analysis machine

AU - Steffen, Bernhard

AU - Claßen, Andreas

AU - Klein, Marion

AU - Knoop, Jens

AU - Margaria, Tiziana

PY - 1995

Y1 - 1995

N2 - We present a fixpoint-analysis machine, for the efficient computation of homogeneous, hierarchical, and alternating fixpoints over regular, context-free/push-down and macro models. Applications of such fixpoint computations include intra- and interprocedural data flow analysis, model checking for various temporal logics, and the verification of behavioural relations between distributed systems. The fixpoint-analysis machine identifies an adequate (parameterized) level for a uniform treatment of all those problems, which, despite its uniformity, outperforms the ‘standard iteration based’ special purpose tools usually by factors around 10, even if the additional compilation time is taken into account.

AB - We present a fixpoint-analysis machine, for the efficient computation of homogeneous, hierarchical, and alternating fixpoints over regular, context-free/push-down and macro models. Applications of such fixpoint computations include intra- and interprocedural data flow analysis, model checking for various temporal logics, and the verification of behavioural relations between distributed systems. The fixpoint-analysis machine identifies an adequate (parameterized) level for a uniform treatment of all those problems, which, despite its uniformity, outperforms the ‘standard iteration based’ special purpose tools usually by factors around 10, even if the additional compilation time is taken into account.

UR - http://www.scopus.com/inward/record.url?scp=84947753987&partnerID=8YFLogxK

U2 - 10.1007/3-540-60218-6_6

DO - 10.1007/3-540-60218-6_6

M3 - Conference contribution

AN - SCOPUS:84947753987

SN - 3540602186

SN - 9783540602187

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 72

EP - 87

BT - CONCUR 1995

A2 - Lee, Insup

A2 - Smolka, Scott A.

PB - Springer Verlag

T2 - 6th International Conference on Concurrency Theory, CONCUR 1995

Y2 - 21 August 1995 through 24 August 1995

ER -

Steffen B, Claßen A, Klein M, Knoop J, Margaria T. The fixpoint-analysis machine. In Lee I, Smolka SA, editors, CONCUR 1995: Concurrency Theory - 6th International Conference, Proceedings. Springer Verlag. 1995. p. 72-87. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-60218-6_6

The fixpoint-analysis machine

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this