Transformational Verification of Quicksort Emanuele De Angelis CNR-IASI Via dei Taurini 19, 00185 Roma, Italy [email protected] DEC, University “G. d’Annunzio” of Chieti-Pescara Viale Pindaro 42, 65127 Pescara, Italy CNR-IASI Via dei Taurini 19, 00185 Roma, Italy Fabio Fioravanti DEC, University “G. d’Annunzio” of Chieti-Pescara Viale Pindaro 42, 65127 Pescara, Italy [email protected] CNR-IASI Via dei Taurini 19, 00185 Roma, Italy CNR-IASI Via dei Taurini 19, 00185 Roma, Italy Maurizio Proietti CNR-IASI Via dei Taurini 19, 00185 Roma, Italy [email protected] Abstract 1 From Program Transformation to Program Verification 2 Program Verification via Constrained Horn Clause Transformation 3 Specification of Quicksort with Parameterized Catamorphisms 4 Removing List Arguments 5 Related Work and Conclusions Appendix