Compositional circular assume-guarantee rules cannot be sound and complete

Patrick Maier

Research output: Chapter in Book/Report/Conference proceedingConference 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 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
Country/TerritoryPoland
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