Compositional circular assume-guarantee rules cannot be sound and complete

Patrick Maier

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 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 languageEnglish
Title of host publicationFoundations of Software Science and Computational Structures
Subtitle of host publication6th 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
PublisherSpringer
Pages343-357
Number of pages15
Volume2620
ISBN (Electronic)978-3-540-36576-1
ISBN (Print)978-3-540-00897-2
DOIs
Publication statusPublished - Apr 2003
Event6th International Conference on Foundations of Software Science and Computation Structures - Warsaw, Poland
Duration: 7 Apr 200311 Apr 2003

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743

Conference

Conference6th International Conference on Foundations of Software Science and Computation Structures
Abbreviated titleFOSSACS 2003
CountryPoland
CityWarsaw
Period7/04/0311/04/03

Keywords

  • compositional verification
  • assume-guarantee reasoning
  • completeness

Fingerprint Dive into the research topics of 'Compositional circular assume-guarantee rules cannot be sound and complete'. Together they form a unique fingerprint.

  • 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