Jean-Paul Bodeveix, Mamoun Filali: Reduction and Quantifier Elimination Techniques for Program Validation. Formal Methods Syst. Des. 20(1): 69-89 (2002)