English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT
Add to Basket
  Local TagsRelease HistoryDetailsSummary

Released
Report

Compositional circular assume-guarantee rules cannot be sound and complete

MPS-Authors
/persons/resource/persons44970

Maier,  Patrick
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

MPI-I-2003-2-001.pdf
(Any fulltext), 293KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Maier, P.(2003). Compositional circular assume-guarantee rules cannot be sound and complete (MPI-I-2003-2-001). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: https://hdl.handle.net/11858/00-001M-0000-0014-6B04-7
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.