KIT | KIT-Bibliothek | Impressum
Open Access Logo
§
Volltext
DOI: 10.5445/IR/1000051022

Relational Reasoning - Constraint Solving, Deduction, and Program Verification

El Ghazi, Aboubakr Achraf

Abstract:
This dissertation exploits the formal methods paradigm in which the software system and its specification are transformed to a logical formula, such that the formula is valid iff the specification is correct. The thesis provides a reasoning framework for the verification of software systems against relational specifications written in a first-order relational logic. The system description can be given either at the abstract relational level or at the detailed implementation level.


Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Publikationstyp Hochschulschrift
Jahr 2015
Sprache Englisch
Identifikator URN: urn:nbn:de:swb:90-510220
KITopen ID: 1000051022
Verlag Karlsruhe
Abschlussart Dissertation
Fakultät Fakultät für Informatik (INFORMATIK)
Institut Institut für Theoretische Informatik (ITI)
Prüfungsdaten 27.10.2015
Referent/Betreuer Prof. M. Taghdiri
Schlagworte Formal Methods, Specification, Verification, Relational Logics, Relational Reasoning, Constraint Solving
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page