Formalization of variables access constraints to support compositionality of liveness properties

I. S.W.B. Prasetya

doi:10.1007/3-540-57826-9_145

Formalization of variables access constraints to support compositionality of liveness properties

I. S.W.B. Prasetya^*

^*Corresponding author for this work

Sub Software Technology

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

Abstract

Because reasoning about programs’ llveness behavior is difficult people become interested in the potential of theorem provers to aid verification. In extending a theorem prover with a lifeness logic it would be nice if compositionality is also supported since it is a property of a great practical interest: it allows modularity in design. However, a straightforward extension that only embodies the essence of the logic will fail to do so. In implementing such an extension we should therefore be aware of the technical details required for compositionality. In particular, compositionality of progress under parallel composition depends on the concept of variable accessibility. Therefore, this concept has to be explicitly present in the extension. This paper is about the formalization of access constraints to support compositionality.

Original language	English
Title of host publication	Higher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings
Editors	Jeffrey J. Joyce, Carl-Johan H. Seger
Publisher	Springer
Pages	324-337
Number of pages	14
ISBN (Print)	9783540578260
DOIs	https://doi.org/10.1007/3-540-57826-9_145
Publication status	Published - 1994
Event	6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993 - Vancouver, Canada Duration: 11 Aug 1993 → 13 Aug 1993

Publication series

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

Conference

Conference	6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993
Country/Territory	Canada
City	Vancouver
Period	11/08/93 → 13/08/93

Bibliographical note

Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1994.

Access to Document

10.1007/3-540-57826-9_145

Cite this

Prasetya, I. S. W. B. (1994). Formalization of variables access constraints to support compositionality of liveness properties. In J. J. Joyce, & C.-J. H. Seger (Eds.), Higher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings (pp. 324-337). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 780 LNCS). Springer. https://doi.org/10.1007/3-540-57826-9_145

Prasetya, I. S.W.B. / Formalization of variables access constraints to support compositionality of liveness properties. Higher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings. editor / Jeffrey J. Joyce ; Carl-Johan H. Seger. Springer, 1994. pp. 324-337 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{31983799212348a58312dac3501269ee,

title = "Formalization of variables access constraints to support compositionality of liveness properties",

abstract = "Because reasoning about programs{\textquoteright} llveness behavior is difficult people become interested in the potential of theorem provers to aid verification. In extending a theorem prover with a lifeness logic it would be nice if compositionality is also supported since it is a property of a great practical interest: it allows modularity in design. However, a straightforward extension that only embodies the essence of the logic will fail to do so. In implementing such an extension we should therefore be aware of the technical details required for compositionality. In particular, compositionality of progress under parallel composition depends on the concept of variable accessibility. Therefore, this concept has to be explicitly present in the extension. This paper is about the formalization of access constraints to support compositionality.",

author = "Prasetya, {I. S.W.B.}",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1994.; 6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993 ; Conference date: 11-08-1993 Through 13-08-1993",

year = "1994",

doi = "10.1007/3-540-57826-9_145",

language = "English",

isbn = "9783540578260",

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

publisher = "Springer",

pages = "324--337",

editor = "Joyce, {Jeffrey J.} and Seger, {Carl-Johan H.}",

booktitle = "Higher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings",

}

Prasetya, ISWB 1994, Formalization of variables access constraints to support compositionality of liveness properties. in JJ Joyce & C-JH Seger (eds), Higher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 780 LNCS, Springer, pp. 324-337, 6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993, Vancouver, Canada, 11/08/93. https://doi.org/10.1007/3-540-57826-9_145

Formalization of variables access constraints to support compositionality of liveness properties. / Prasetya, I. S.W.B.
Higher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings. ed. / Jeffrey J. Joyce; Carl-Johan H. Seger. Springer, 1994. p. 324-337 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 780 LNCS).

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

TY - GEN

T1 - Formalization of variables access constraints to support compositionality of liveness properties

AU - Prasetya, I. S.W.B.

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1994.

PY - 1994

Y1 - 1994

N2 - Because reasoning about programs’ llveness behavior is difficult people become interested in the potential of theorem provers to aid verification. In extending a theorem prover with a lifeness logic it would be nice if compositionality is also supported since it is a property of a great practical interest: it allows modularity in design. However, a straightforward extension that only embodies the essence of the logic will fail to do so. In implementing such an extension we should therefore be aware of the technical details required for compositionality. In particular, compositionality of progress under parallel composition depends on the concept of variable accessibility. Therefore, this concept has to be explicitly present in the extension. This paper is about the formalization of access constraints to support compositionality.

AB - Because reasoning about programs’ llveness behavior is difficult people become interested in the potential of theorem provers to aid verification. In extending a theorem prover with a lifeness logic it would be nice if compositionality is also supported since it is a property of a great practical interest: it allows modularity in design. However, a straightforward extension that only embodies the essence of the logic will fail to do so. In implementing such an extension we should therefore be aware of the technical details required for compositionality. In particular, compositionality of progress under parallel composition depends on the concept of variable accessibility. Therefore, this concept has to be explicitly present in the extension. This paper is about the formalization of access constraints to support compositionality.

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

U2 - 10.1007/3-540-57826-9_145

DO - 10.1007/3-540-57826-9_145

M3 - Conference contribution

AN - SCOPUS:0011240794

SN - 9783540578260

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

SP - 324

EP - 337

BT - Higher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings

A2 - Joyce, Jeffrey J.

A2 - Seger, Carl-Johan H.

PB - Springer

T2 - 6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, HUG 1993

Y2 - 11 August 1993 through 13 August 1993

ER -

Prasetya ISWB. Formalization of variables access constraints to support compositionality of liveness properties. In Joyce JJ, Seger CJH, editors, Higher Order Logic Theorem Proving and Its Applications - 6th International Workshop, HUG 1993, Proceedings. Springer. 1994. p. 324-337. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-57826-9_145

Formalization of variables access constraints to support compositionality of liveness properties

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Other files and links

Fingerprint

Cite this