title: Sûreté (propriété de programme)
text: # 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é.
  
  