MPI-INF Logo
Publications

Server    halma.mpi-inf.mpg.de

Proceedings Article, Paper


@InProceedings
Beitrag in Tagungsband, Workshop
Author, Editor
Author(s):
Maier, Patrickdblp
Editor(s):
Orejas, Fernando
Spirakis, Paul G.
van Leeuwen, Jan		dblp
dblp
dblp
BibTeX cite key*:
Maier2001
Title, Booktitle
Title*:
A Set-Theoretic Framework for Assume-Guarantee Reasoning
Booktitle*:
Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP-2001)
Event, URLs
Conference URL::
http://www.cti.gr/icalp01
Downloading URL:
Event Address*:
Crete, Greece
Language:
English
Event Date*
(no longer used):
Organization:
Event Start Date:
8 July 2001
Event End Date:
12 July 2001
Publisher
Name*:
Springer
URL:
Address*:
Berlin, Germany
Type:
Vol, No, Year, pp.
Series:
Lecture Notes in Computer Science
Volume:
2076
Number:
Month:
July
Pages:
821-834
Year*:
2001
VG Wort Pages:
14
ISBN/ISSN:
3-540-42287-0
Sequence Number:
DOI:
Note, Abstract, ©
(LaTeX) Abstract:
We present a circular assume-guarantee rule in an abstract setting (of
sets over a partially-ordered domain). The rule has a mathematically
concise side condition. Now, in order to prove an assume-guarantee
rule in a concrete setting, all we need to do is to is to instantiate
the abstract setting and check the side condition; i.e., we need not
redo the notorious circularity argument again. We use this framework
to prove a new assume-guarantee rule for Kripke structures. That rule
generalizes existing assume-guarantee rules for other settings such as
Reactive Modules or Mealy machines.
Keywords:
Compositional Verification, Assume-Guarantee Reasoning, Trace Semantics
Download
Access Level:
Public

Correlation
MPG Unit:
Max-Planck-Institut für Informatik
MPG Subunit:
Programming Logics Group
Audience:
experts only
Appearance:
MPG publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:
@INPROCEEDINGS{Maier2001,
AUTHOR = {Maier, Patrick},
 EDITOR = {Orejas, Fernando and Spirakis, Paul G. and van Leeuwen, Jan},
 TITLE = {A Set-Theoretic Framework for Assume-Guarantee Reasoning},
 BOOKTITLE = {Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP-2001)},
 PUBLISHER = {Springer},
 YEAR = {2001},
 VOLUME = {2076},
 PAGES = {821--834},
 SERIES = {Lecture Notes in Computer Science},
 ADDRESS = {Crete, Greece},
 MONTH = {July},
 ISBN = {3-540-42287-0},
}

Entry last modified by Patrick Maier, 03/12/2010
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Patrick Maier		Created
08/21/2001 04:55:07 PM
Revisions
2.
1.
0.

Editor(s)
Patrick Maier
Uwe Brahm
Patrick Maier

Edit Dates
05/03/2004 08:29:39 PM
31.03.2002 18:15:37
21/08/2001 16:55:07