Comment s'assurer qu'un programme informatique a été correctement écrit ? Lorsque la fiabilité est indispensable pour éviter des accidents, on fait appel à une approche située entre l'informatique et les mathématiques.