Souvent utilisé dans le test de circuits informatiques et de logiciels, vérification formelle, c'est quand la fonction de ces systèmes est analysée à l'aide de formules mathématiques. Dans le cas du développement de logiciels, le processus est généralement utilisé pour indiquer si le programme fonctionne correctement, basée sur un modèle préétabli. Parfois, le modèle théorique est avérée insatisfaisante. En plus du code source du logiciel, la vérification formelle peut être utilisée dans le développement de circuits combinatoires, qui sont utilisés pour effectuer des calculs dans les ordinateurs, ainsi que des mémoires d'ordinateur. Les différentes approches incluent après-coup de vérification, la vérification en parallèle, et la vérification intégrée, en plus de diverses méthodes.
Les procédures mathématiques pour les calculs, appelés algorithmes, sont utilisés dans la vérification formelle de tester les fonctions des produits à chaque étape du développement. Les développeurs de logiciels peuvent trouver des erreurs ou des bugs à la fois dans le code source et le modèle utilisé pour le construire en premier lieu. Parfois, des changements fondamentaux dans la façon dont le code est écrit peut être faite avant une erreur de conception affecte le résultat final. L'étape de vérification permet généralement de déterminer si le produit fait ce qui était prévu de le faire, et répond aux spécifications de l'application, il est pour.
La vérification formelle peut se produire quand un produit est terminé, ce qui est appelé après-coup de vérification. Une méthode standard, utilisé tout au long du processus de conception et de développement, ne sont pas analysées jusqu'à ce que le système est terminée. Localisation de graves erreurs à ce stade conduit souvent à des révisions coûteuses et de longue haleine. Développement et vérification peut également être effectuée par deux équipes distinctes pour la vérification en parallèle. Grâce à l'intercommunication, les développeurs peuvent se concentrer sur des tâches indépendantes au cours du processus de conception.
La vérification intégrée, c'est quand une équipe effectue la mise au point et l'évaluation requise. Des concepts mathématiques complexes sont souvent utilisés pour vérifier les capacités du produit en cours de route. Les méthodes de vérification formelle varient selon les projets, mais on a souvent utilisé est le model checking. Un modèle de matériel ou de logiciel se compose de diverses propriétés que les concepteurs veulent dans le produit fini. Le modèle et le système peut être vérifiée périodiquement pour voir si les propriétés correspondent.
Une autre technique consiste en la vérification formelle à l'aide de formules mathématiques et de la logique pour représenter un système et ses propriétés. Règles définies dans un système formel se trouvent généralement dans la logique. Ces deux techniques utilisent différents moyens pour déterminer si une spécification particulière d'un produit est atteint. Les développeurs peuvent utiliser différents types de logiciels dans le processus de vérification formelle, chacun adapté à un système ou langage de programmation.