Sûreté (propriété de programme)
# Sûreté (propriété de programme)

En informatique, notamment en méthode formelle, la sûreté (en anglais : safety) est pour un programme le fait de ne pas sortir d'un certain ensemble d'états. Notamment, on exclut la sortie d'un ensemble d'états « sûrs » (les autres indiquant des erreurs).

C'est avec la vivacité l'une des deux propriétés théoriques fondamentales des programmes informatiques.

## Logique temporelle

En logique temporelle linéaire (LTL), en représentant toute exécution par un mot (potentiellement infini), une propriété de sûreté est associée à des « mauvais préfixes » qui sont des mots finis qui la violent, autrement dit, tout mot commençant par un tel préfixe viole ladite propriété. On caractérise ainsi une propriété de sûreté.

