h1

h2

h3

h4

h5
h6
http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png

Integrating virtual substitution into strategic SMT solving = Integration der virtuellen Substitution in strategisches SMT Solving



Verantwortlichkeitsangabevorgelegt von Diplom-Informatiker Florian Corzilius

ImpressumAachen 2016

Umfang1 Online-Ressource (IX, 186 Seiten) : Illustrationen, Diagramme


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

  1. Lehrstuhl für Informatik 2 (Softwaremodellierung und Verifikation) (121310)
  2. Lehr- und Forschungsgebiet Theorie Hybrider Systeme (123420)
  3. Fachgruppe Informatik (120000)

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:
Download fulltext PDF Download fulltext 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

 GO


OpenAccess

QR Code for this record

The record appears in these collections:
Document types > Theses > Ph.D. Theses
Faculty of Mathematics, Computer Science and Natural Sciences (Fac.1) > Department of Computer Science
Publication server / Open Access
Public records
Publications database
120000
121310
123420

 Record created 2017-04-13, last modified 2023-04-08