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

MPI-INF RG1 Publications :: Thesis :: Ihlemann, Carsten

MPI-INF RG1 Publications
Show all entries of:this year (2019)last year (2018)two years ago (2017)Open in Notes
Action:login to update  Library locked

Thesis - Doctoral dissertation | @PhdThesis | Doktorarbeit

Author(s)*:Ihlemann, Carsten
BibTeX citekey*:IhlemannDiss2010

Title, School
Title*:Reasoning in Combinations of Theories
School:Universität des Saarlandes
Type of Thesis*:Doctoral dissertation

Publishers Name:Universität des Saarlandes
Publishers Address:Saarbrücken

Note, Abstract, Copyright
LaTeX Abstract:\section*{Abstract}

Verification problems are often expressed in a language which mixes several theories.
A natural question to ask is whether one can use decision procedures for individual theories to construct a decision procedure for the union theory.
In the cases where this is possible one has a powerful method at hand to handle complex theories effectively.

The setup considered in this thesis is that of one base theory which is extended by one or more theories.
The question is if and when a given ground satisfiability problem in the extended setting can be
effectively reduced to an equi-satisfiable
over the base theory. A case where this reductive approach is always possible is that of so-called \emph{local theory extensions.}

The theory of local extensions is developed and some applications concerning monotone functions are given.
Then the theory of local theory extensions is generalized in order to deal with data structures that
exhibit local behavior.
It will be shown that a suitable fragment of both the theory of arrays and the theory of pointers
is local in this broader sense.
Finally, the case of more than one theory extension is discussed.
In particular, a \emph{modularity} result is given that under certain circumstances the locality of each of the extensions
lifts to locality of the entire extension.

The reductive approach outlined above has become particularly relevant
in recent years due to the rise of powerful solvers for background
theories common in verification tasks. These so-called SMT-solvers
effectively handle theories such as real linear or integer arithmetic.
As part of this thesis, a program called \emph{\mbox{H-PILoT}} was
implemented which carries out reductive reasoning for local theory
extensions. H-PILoT found applications in mathematics, multiple-valued
logics, data-structures and reasoning in complex systems.

Keywords:Verification, Theorem Proving, Combinations of Theories
Download Access Level:Public
Download File(s):View attachments here:

Referees, Status, Dates
1. Referee:Silvio Ghilardi
2. Referee:Bernd Finkbeiner
Supervisor:Viorica Sofronie-Stokkermans
Date Kolloquium:25 August 2010
Chair Kolloquium:Gert Smolka

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:
AUTHOR = {Ihlemann, Carsten},
TITLE = {Reasoning in Combinations of Theories},
PUBLISHER = {Universität des Saarlandes},
SCHOOL = {Universit{\"a}t des Saarlandes},
YEAR = {2010},
TYPE = {Doctoral dissertation}
PAGES = {176},
ADDRESS = {Saarbr{\"u}cken},
MONTH = {August},

Hide details for Attachment SectionAttachment Section

View attachments here:

Entry last modified by Anja Becker, 02/07/2011
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)

12/20/2010 06:32:38 PM

Anja Becker
Carsten Ihlemann

Edit Date
07.02.2011 13:13:08
12/20/2010 06:32:38 PM