Analyse statique de programmesEn informatique, la notion d’analyse statique de programmes couvre une variété de méthodes utilisées pour obtenir des informations sur le comportement d'un programme lors de son exécution sans réellement l'exécuter. C'est cette dernière restriction qui distingue l'analyse statique des analyses dynamiques (comme le débugage ou le profiling) qui s'attachent, elles, au suivi de l’exécution du programme. L’analyse statique est utilisée pour repérer des erreurs formelles de programmation ou de conception et pour déterminer la facilité ou la difficulté à maintenir le code.
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.
Program analysisIn computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program optimization and program correctness. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what it is supposed to do.
Analyse dynamique de programmesthumb|Logo de Valgrind. Outil permettant de profiler du code. L'analyse dynamique de programme (dynamic program analysis ou DPA), est une forme d'analyse de programme qui nécessite leur exécution. Elle permet d'étudier le comportement d'un programme informatique et les effets de son exécution sur son environnement. Appliquée dans un environnement physique ou virtuel, elle est souvent utilisée pour profiler des programmes. Que ce soit pour retirer des informations sur le temps d'utilisation du processeur, l'utilisation de la mémoire ou encore l'énergie dépensée par le programme.
Vérification formelleIn the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.
Structure de KripkeUne structure de Kripke est un modèle de calcul, proche d'un automate fini non déterministe, inventé par Saul Kripke. Elle est utilisée par exemple dans le model checking pour représenter le comportement d'un système. C'est un graphe orienté dont les nœuds représentent les états accessibles du système et dont les arcs représentent les transitions entre les états. Une fonction d'étiquetage fait correspondre à chaque état un ensemble de propositions logiques vraies dans cet état.
Interprétation abstraiteL'interprétation abstraite est une théorie d'approximation de la sémantique de programmes informatiques fondée sur les fonctions monotones pour ensembles ordonnés, en particulier les treillis (en anglais : lattice). Elle peut être définie comme une exécution partielle d'un programme pour obtenir des informations sur sa sémantique (par exemple, sa structure de contrôle, son flot de données) sans avoir à en faire le traitement complet.
Interprète (informatique)En informatique, un interprète, ou interpréteur , est un outil dont la tâche est d'analyser, de traduire et d'exécuter les programmes écrits dans un langage informatique. On qualifie parfois, , les langages dont les programmes sont généralement exécutés par un interprète de langages interprétés. Un interprète se distingue d’un compilateur par le fait qu’il effectue l’analyse et la traduction nécessaires à l'exécution d’un programme donné non pas une fois pour toutes, mais à chaque exécution de ce programme.
Arbre bicoloreUn arbre bicolore, ou arbre rouge-noir ou arbre rouge et noir est un type particulier d'arbre binaire de recherche équilibré, qui est une structure de données utilisée en informatique théorique. Les arbres bicolores ont été inventés en 1972 par Rudolf Bayer qui les nomme symmetric binary B-trees (littéralement « arbres B binaires symétriques »). Chaque nœud de l'arbre possède en plus de ses données propres un attribut binaire qui est souvent interprété comme sa « couleur » (rouge ou noir).
Test (informatique)vignette|Une programmeuse écrivant du code Java avec JUnit. En informatique, un test désigne une procédure de vérification partielle d'un système. Son objectif principal est d'identifier un nombre maximal de comportements problématiques du logiciel. Il permet ainsi, dès lors que les problèmes identifiés seront corrigés, d'en augmenter la qualité. D'une manière plus générale, le test désigne toutes les activités qui consistent à rechercher des informations quant à la qualité du système afin de permettre la prise de décisions.
