Je présenterai une approche modulaire et incrémentale des preuves de terminaison de systèmes de récriture de grande taille ainsi que son extension au cas de la récriture modulo associativité et commutativité. Les critères qui en sont issus permettent la preuve automatique de terminaison sur des systèmes pouvant comporter plusieurs centaines de règles. J'illustrerai mon propos à l'aide d'exemples traités de façon complètement automatique par l'outil CiME où sont implantées ces techniques.
J'aborderai ensuite la vérification de programmes Java en présentant une approche qui permet la vérification de programmes Java annotés en JML avec différents prouveurs/assistants de preuve. Elle procède par plongement superficiel du code source dans le langage du générateur d'obligations de preuve Why. La méthode demande, d'une part, de traduire correctement les annotations dans le langage logique et, d'autre part, de définir un modèle des objets.