MPI-INF RG1 Publications: Report

Title*:	On hierarchical reasoning in combinations of theories
Institution*:	Sonderforschungsbereich/Transregio 14 AVACS (Automatic Verification and Analysis of Complex Systems)
Publishers or Institutions Address*:	Saarbrücken
Type:	Technical Report

No, Year, pp.,

Number*:	ATR 60	Pages*:	26
Month:	August	VG Wort Pages*:
Year*:	2010	ISBN/ISSN:	1860-9821

DOI:

Note:
(LaTeX) Abstract:	In this paper we study theory combinations over non-disjoint signatures in which hierarchical and modular reasoning is possible. We use a notion of locality of a theory extension parameterized by a closure operator on ground terms. We give criteria for recognizing these types of theory extensions. We then show that combinations of extensions of theories which are local in this extended sense have also a locality property and hence allow modular and hierarchical reasoning. We thus obtain parameterized decidability and complexity results for many (combinations of) theories important in verification.
Categories / Keywords:
Copyright Message:
HyperLinks / References / URLs:
Personal Comments:
File Upload:
Download Access Level:	Public

Correlation

MPG Unit:	Max-Planck-Institut für Informatik

MPG Subunit:	Automation of Logic
Appearance:	MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort

BibTeX Entry:

@TECHREPORT{Ihlemann-Sofronie-Stokkermans-atr60-2010,
AUTHOR = {Ihlemann, Carsten and Sofronie-Stokkermans, Viorica},
EDITOR = {Bernd, Becker and Damm, Werner and Fr{\"a}nzle, Martin and Olderog, Ernst-R{\"u}diger and Podelski, Andreas and Wilhelm, Reinhard},
TITLE = {On hierarchical reasoning in combinations of theories},
YEAR = {2010},
TYPE = {Technical Report},
INSTITUTION = {Sonderforschungsbereich/Transregio 14 AVACS (Automatic Verification and Analysis of Complex Systems)},
NUMBER = {ATR 60},
PAGES = {26},
ADDRESS = {Saarbr{\"u}cken},
MONTH = {August},
ISBN = {1860-9821},
}

Entry last modified by Anja Becker, 03/15/2011

Edit History (please click the blue arrow to see the details)

Attachment Section