Vérification de modèlesthumb|308x308px|Principe du model checking. En informatique, la vérification de modèles, ou model checking en anglais, est le problème suivant : vérifier si le modèle d'un système (souvent informatique ou électronique) satisfait une propriété. Par exemple, on souhaite vérifier qu'un programme ne se bloque pas, qu'une variable n'est jamais nulle, etc. Généralement, la propriété est écrite dans un langage, souvent en logique temporelle. La vérification est généralement faite de manière automatique.
Anneau de protectionUn anneau de protection (ring en anglais) est l’un des niveaux de privilèges imposés par l’architecture d’un processeur. De nombreuses architectures modernes de processeurs (architectures parmi lesquelles on trouve le populaire Intel x86) incluent une certaine forme de protection en anneau, bien que les logiciels d’exploitation ne l’exploitent pas toujours entièrement. Les rings étaient parmi les concepts les plus révolutionnaires mis en œuvre par le système d’exploitation Multics, un prédécesseur fortement sécurisé de la famille actuelle des systèmes d’exploitation UNIX.
