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.

@phdthesis{ElGhazi2015Phd,
author = {Aboubakr Achraf {El Ghazi}},
title = {Relational Reasoning - Constraint Solving, Deduction, and
Program Verification},
school = {Karlsruhe Institute of Technology},
year = {2015},
month = oct,
doi = {10.5445/IR/1000051022},
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.}
}