Durante estos años de experiencia hemos podido comprobar que los alumnos siempre reclaman libros que no se extiendan tanto en teoría y que parte del texto lo completen con ejercicios resueltos. Como respuesta a este reclamo nace este libro, que se presenta como un complemento a las obras ya existentes, y cuyo objetivo principal es el de ayudar a los alumnos en el aprendizaje de esta materia compleja, como es la veriÿcación formal de algoritmos. Es un texto eminentemente práctico, cuya ÿnalidad es la de ofrecer al alumno una guía para comprender y aÿanzar los conocimientos teóricos a través de la resolución de ejercicios de elevada diÿcultad. Está dirigida a estudiantes con ciertos conocimientos sobre el tema y que le permitirá profundizar aún más mediante el autoaprendizaje a través de la práctica de ejercicios.En esta obra se presenta la demostración formal de la corrección de algoritmos de cierta complejidad, los cuales contienen varias estructuras de control. Es por ello que se aconseja comenzar el estudio con el libro que le precede, Veriÿcación formal de algoritmos. Ejercicios resueltos, que comienza con conceptos básicos y continúa con la corrección de numerosos fragmentos de código, tanto iterativos como recursivos. La descripción de algoritmos se realiza en pseudocódigo, para que las demostraciones sean independientes del lenguaje de programación utilizado, aunque se sigue el paradigma de lenguajes imperativos.