Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

Publications Master Template :: Thesis :: Maier, Patrick

Publications Master Template
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update

Thesis - Doctoral dissertation | @PhdThesis | Doktorarbeit

Author(s)*:Maier, Patrick
BibTeX citekey*:Maier2003

Title, School
Title*:A Lattice-Theoretic Framework For Circular Assume-Guarantee Reasoning
School:Universität des Saarlandes
Type of Thesis*:Doctoral dissertation

Note, Abstract, Copyright
LaTeX Abstract:We develop an abstract lattice-theoretic framework within which

we study soundness and other properties of circular assume-
guarantee (A-G) rules constrained by side conditions. We
identify a particular side condition, non-blockingness, which
admits an intelligible inductive proof of the soundness of
circular A-G reasoning. Besides, conditional circular rules
based on non-blockingness turn out to be complete in various
senses and stronger than a large class of sound conditional A-G
rules. In this respect, our framework enlightens the foundations
of circular A-G reasoning.
Due to its abstractness, the framework can be instantiated to
many concrete settings. We show several known circular A-G rules
for compositional verification to be instances of our generic
rules. Thus, we do the circularity-breaking inductive argument
once to establish soundness of our generic rules, which then
implies soundness of all the instances without resorting to
technically complicated circularity-breaking arguments for each
single rule. In this respect, our framework unifies many
approaches to circular A-G reasoning and provides a starting
point for the systematic development of new circular A-G rules.

Referees, Status, Dates
1. Referee:Prof. Dr. Andreas Podelski
2. Referee:Dr. Sriram K. Rajamani
Supervisor:Prof. Dr. Andreas Podelski
Date Kolloquium:23 July 2003
Chair Kolloquium:Prof. Dr. Bernd Finkbeiner

MPG Unit:Max-Planck-Institut für Informatik
MPG Subunit:Programming Logics Group
Audience:not specified
Appearance:MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, CCL bibliography

BibTeX Entry:
AUTHOR = {Maier, Patrick},
TITLE = {A Lattice-Theoretic Framework For Circular Assume-Guarantee Reasoning},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {2003},
TYPE = {Doctoral dissertation}
MONTH = {July},

Entry last modified by Patrick Maier, 01/28/2008
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)

Patrick Maier
06/29/2004 07:14:12 PM

Patrick Maier

Edit Date
06/29/2004 07:14:13 PM