Compositional circular assume-guarantee rules cannot be sound and complete

Patrick Maier

doi:10.1007/3-540-36576-1_22

Compositional circular assume-guarantee rules cannot be sound and complete

Patrick Maier

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

15 Citations (Scopus)

Abstract

Circular assume-guarantee reasoning is used for the compositional verification of concurrent systems. Its soundness has been studied in depth, perhaps because circularity makes it anything but obvious. In this paper, we investigate completeness. We show that compositional circular assume-guarantee rules cannot be both sound and complete.

Original language	English
Title of host publication	Foundations of Software Science and Computational Structures
Subtitle of host publication	6th International Conference, FOSSACS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003; Warsaw, Poland, April 7–11, 2003; Proceedings
Publisher	Springer
Pages	343-357
Number of pages	15
Volume	2620
ISBN (Electronic)	978-3-540-36576-1
ISBN (Print)	978-3-540-00897-2
DOIs	https://doi.org/10.1007/3-540-36576-1_22
Publication status	Published - Apr 2003
Event	6th International Conference on Foundations of Software Science and Computation Structures - Warsaw, Poland Duration: 7 Apr 2003 → 11 Apr 2003

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
ISSN (Print)	0302-9743

Conference

Conference	6th International Conference on Foundations of Software Science and Computation Structures
Abbreviated title	FOSSACS 2003
Country/Territory	Poland
City	Warsaw
Period	7/04/03 → 11/04/03

Keywords

compositional verification
assume-guarantee reasoning
completeness

Access to Document

10.1007/3-540-36576-1_22

Cite this

Maier, P. (2003). Compositional circular assume-guarantee rules cannot be sound and complete. In Foundations of Software Science and Computational Structures: 6th International Conference, FOSSACS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003; Warsaw, Poland, April 7–11, 2003; Proceedings (Vol. 2620, pp. 343-357). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/3-540-36576-1_22

Maier, Patrick. / Compositional circular assume-guarantee rules cannot be sound and complete. Foundations of Software Science and Computational Structures: 6th International Conference, FOSSACS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003; Warsaw, Poland, April 7–11, 2003; Proceedings. Vol. 2620 Springer, 2003. pp. 343-357 (Lecture Notes in Computer Science).

@inproceedings{3d26fa4c36494814aaab9cc2bc403b2e,

title = "Compositional circular assume-guarantee rules cannot be sound and complete",

abstract = "Circular assume-guarantee reasoning is used for the compositional verification of concurrent systems. Its soundness has been studied in depth, perhaps because circularity makes it anything but obvious. In this paper, we investigate completeness. We show that compositional circular assume-guarantee rules cannot be both sound and complete.",

keywords = "compositional verification, assume-guarantee reasoning, completeness",

author = "Patrick Maier",

year = "2003",

month = apr,

doi = "10.1007/3-540-36576-1_22",

language = "English",

isbn = "978-3-540-00897-2",

volume = "2620",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "343--357",

booktitle = "Foundations of Software Science and Computational Structures",

note = "6th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2003 ; Conference date: 07-04-2003 Through 11-04-2003",

}

Maier, P 2003, Compositional circular assume-guarantee rules cannot be sound and complete. in Foundations of Software Science and Computational Structures: 6th International Conference, FOSSACS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003; Warsaw, Poland, April 7–11, 2003; Proceedings. vol. 2620, Lecture Notes in Computer Science, Springer, pp. 343-357, 6th International Conference on Foundations of Software Science and Computation Structures, Warsaw, Poland, 7/04/03. https://doi.org/10.1007/3-540-36576-1_22

Compositional circular assume-guarantee rules cannot be sound and complete. / Maier, Patrick.

Foundations of Software Science and Computational Structures: 6th International Conference, FOSSACS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003; Warsaw, Poland, April 7–11, 2003; Proceedings. Vol. 2620 Springer, 2003. p. 343-357 (Lecture Notes in Computer Science).

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

TY - GEN

T1 - Compositional circular assume-guarantee rules cannot be sound and complete

AU - Maier, Patrick

PY - 2003/4

Y1 - 2003/4

N2 - Circular assume-guarantee reasoning is used for the compositional verification of concurrent systems. Its soundness has been studied in depth, perhaps because circularity makes it anything but obvious. In this paper, we investigate completeness. We show that compositional circular assume-guarantee rules cannot be both sound and complete.

AB - Circular assume-guarantee reasoning is used for the compositional verification of concurrent systems. Its soundness has been studied in depth, perhaps because circularity makes it anything but obvious. In this paper, we investigate completeness. We show that compositional circular assume-guarantee rules cannot be both sound and complete.

KW - compositional verification

KW - assume-guarantee reasoning

KW - completeness

U2 - 10.1007/3-540-36576-1_22

DO - 10.1007/3-540-36576-1_22

M3 - Conference contribution

SN - 978-3-540-00897-2

VL - 2620

T3 - Lecture Notes in Computer Science

SP - 343

EP - 357

BT - Foundations of Software Science and Computational Structures

PB - Springer

T2 - 6th International Conference on Foundations of Software Science and Computation Structures

Y2 - 7 April 2003 through 11 April 2003

ER -

Maier P. Compositional circular assume-guarantee rules cannot be sound and complete. In Foundations of Software Science and Computational Structures: 6th International Conference, FOSSACS 2003, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2003; Warsaw, Poland, April 7–11, 2003; Proceedings. Vol. 2620. Springer. 2003. p. 343-357. (Lecture Notes in Computer Science). doi: 10.1007/3-540-36576-1_22

Compositional circular assume-guarantee rules cannot be sound and complete

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this