Olivier Ponsini. Des programmes impératifs vers la logique équationnelle pour la vérification. (From imperative programs to equational logic for correctness verification). PhD thesis, University of Nice Sophia Antipolis, France, 2005. [doi]
Abstract is missing.