2016 & 2017
Dissertation, RWTH Aachen University, 2016
Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2017
Genehmigende Fakultät
Fak01
Hauptberichter/Gutachter
;
Tag der mündlichen Prüfung/Habilitation
2016-10-21
Online
DOI: 10.18154/RWTH-2017-03775
URL: http://publications.rwth-aachen.de/record/688379/files/688379.pdf
URL: http://publications.rwth-aachen.de/record/688379/files/688379.pdf?subformat=pdfa
Einrichtungen
Inhaltliche Beschreibung (Schlagwörter)
SMT solving (frei) ; virtual substitution (frei) ; nonlinear real arithmetic (frei) ; nonlinear integer arithmetic (frei) ; theory solver (frei)
Thematische Einordnung (Klassifikation)
DDC: 004
Kurzfassung
Diese Doktorarbeit behandelt die Integrierung reell-algebraischer Prozeduren als Theory-Solver in Satisfiability-Modulo-Theories-Solver (SMT-Solver), um nichtlineare reell- und ganzzahlig-arithmetische Formeln auf Erfüllbarkeit zu überprüfen. Es gibt viele Prozeduren, welche sich hierfür anbieten, und wir streben ein generelles Framework an, mit dem man diese auswählen und kombinieren kann. Der Hauptteil dieser Doktorarbeit beschäftigt sich mit einem spezifischen Beispiel für die obengenannte Integrierung: der Virtual-Substitution-Methode. Hierbei wird diese Methode auch bezüglich der Erfüllbarkeitsüberprüfung optimiert und auf die Anwendbarkeit auf ganzzahlige Arithmetik erweitert.This thesis addresses the integration of real algebraic procedures as theory solvers into satisfiability modulo theories (SMT) solvers, in order to check non-linear real- and integer-arithmetic formulas for satisfiability. There are plenty of procedures to choose from and we aim for a general framework that allows us to select and combine them. The main part of this thesis concerns one specific example of the aforementioned integration: the virtual substitution method. Here we also optimize this method with respect to satisfiability checking and extend it such that it can be used for integer arithmetic.
OpenAccess:
PDF PDF (PDFA)
(additional files)
Dokumenttyp
Dissertation / PhD Thesis
Format
online
Sprache
English
Externe Identnummern
HBZ: HT019306857
Interne Identnummern
RWTH-2017-03775
Datensatz-ID: 688379
Beteiligte Länder
Germany