Relational Reasoning - Constraint Solving, Deduction, and Program Verification

@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.}
}