La mémoire tampon est une zone de stockage temporaire dans la mémoire vive, qu'un programme réserve pour y placer les données du programme. Cependant, comme le tampon n'est qu'une zone de la mémoire, il est tout à fait possible de s'en échapper, notamment en remplissant entièrement la taille du tampon allouée. Cet article a pour objectif de définir précisément le mécanisme de dépassement de tampon, d'en expliquer les failles de sécurité liées, et de présenter les contributions de Sagar Chaki et Scott Hissam dans leur article *Certifying the Absence of Buffer Overflows* publié en 2006, dans lequel ils proposent une méthode de vérification formelle qui permet de certifier l'absence de dépassement de tampon pour un programme.