Max-Planck-Institut für Informatik
max planck institut
informatik
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
Author(s)*:Maier, Patrick
BibTeX citekey*:Maier2003
Language:English

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


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
Status:Completed
Date Kolloquium:23 July 2003
Chair Kolloquium:Prof. Dr. Bernd Finkbeiner

Correlation
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:
@PHDTHESIS{Maier2003,
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)

Editor(s)
Patrick Maier
Created
06/29/2004 07:14:12 PM
Revision
0.



Editor
Patrick Maier



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