• Refine Query
  • Source
  • Publication year
  • to
  • Language
  • 27
  • 18
  • 3
  • Tagged with
  • 51
  • 51
  • 30
  • 28
  • 26
  • 25
  • 24
  • 24
  • 14
  • 14
  • 12
  • 12
  • 11
  • 9
  • 8
  • About
  • The Global ETD Search service is a free service for researchers to find electronic theses and dissertations. This service is provided by the Networked Digital Library of Theses and Dissertations.
    Our metadata is collected from universities around the world. If you manage a university/consortium/country archive and want to be added, details can be found on the NDLTD website.
31

Domaines numériques abstraits faiblement relationels.

Miné, Antoine 06 December 2004 (has links) (PDF)
Le sujet de cette thèse est le développement de méthodes pour la découverte automatique des propriétés des variables numériques d'un programme. Nous nous plaçons dans le cadre de l'interprétation abstraite et introduisons plusieurs nouveaux domaines numériques, dont celui des octogones, de coût et de précision intermédiaires entre les domaines non relationnels (peu précis) et relationnels (coûteux) existants. Nous présentons leur adaptation à l'analyse des nombres à virgule flottante, jusqu'à présent limitée aux domaines non relationnels. Enfin, nous présentons les méthodes génériques de linéarisation et de propagation symbolique améliorant leur précision pour un surcoût réduit. Les méthodes introduites dans cette thèse ont été intégr! ées à l'analyseur Astrée et appliquées à la preuve d'absence d'erreurs dans le logiciel embarqué critique de commande de vol des avions Airbus A340, justifiant ainsi l'intérêt de nos méthodes pour des cadres d'applications réelles.
32

Analyse de dépendances ML pour les évaluateurs de logiciels critiques.

Benayoun, Vincent 16 May 2014 (has links) (PDF)
Les logiciels critiques nécessitent l'obtention d'une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild'analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d'information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d'outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d'ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d'information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d'uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d'une définition formellede la notion de dépendance, à l'aide de l'assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l'analyse de toléranceaux pannes.
33

Improving the Numerical Accuracy of Floating-Point Programs with Automatic Code Transformation Methods / Amélioration de la précision numérique de programmes basés sur l'arithmétique flottante par les méthodes de transformation automatique

Damouche, Nasrine 12 December 2016 (has links)
Les systèmes critiques basés sur l’arithmétique flottante exigent un processus rigoureux de vérification et de validation pour augmenter notre confiance en leur sureté et leur fiabilité. Malheureusement, les techniques existentes fournissent souvent une surestimation d’erreurs d’arrondi. Nous citons Arian 5 et le missile Patriot comme fameux exemples de désastres causés par les erreurs de calculs. Ces dernières années, plusieurs techniques concernant la transformation d’expressions arithmétiques pour améliorer la précision numérique ont été proposées. Dans ce travail, nous allons une étape plus loin en transformant automatiquement non seulement des expressions arithmétiques mais des programmes complets contenant des affectations, des structures de contrôle et des fonctions. Nous définissons un ensemble de règles de transformation permettant la génération, sous certaines conditions et en un temps polynômial, des expressions pluslarges en appliquant des calculs formels limités, au sein de plusieurs itérations d’une boucle. Par la suite, ces larges expressions sont re-parenthésées pour trouver la meilleure expression améliorant ainsi la précision numérique des calculs de programmes. Notre approche se base sur les techniques d’analyse statique par interprétation abstraite pour sur-rapprocher les erreurs d’arrondi dans les programmes et au moment de la transformation des expressions. Cette approche est implémenté dans notre outil et des résultats expérimentaux sur des algorithmes numériques classiques et des programmes venant du monde d’embarqués sont présentés. / Critical software based on floating-point arithmetic requires rigorous verification and validation process to improve our confidence in their reliability and their safety. Unfortunately available techniques for this task often provide overestimates of the round-off errors. We can cite Arian 5, Patriot rocket as well-known examples of disasters. These last years, several techniques have been proposed concerning the transformation of arithmetic expressions in order to improve their numerical accuracy and, in this work, we go one step further by automatically transforming larger pieces of code containing assignments, control structures and functions. We define a set of transformation rules allowing the generation, under certain conditions and in polynomial time, of larger expressions by performing limited formal computations, possibly among several iterations of a loop. These larger expressions are better suited to improve, by re-parsing, the numerical accuracy of the program results. We use abstract interpretation based static analysis techniques to over-approximate the round-off errors in programs and during the transformation of expressions. A tool has been implemented and experimental results are presented concerning classical numerical algorithms and algorithms for embedded systems.
34

Static analysis of numerical properties in the presence of pointers / Analyse statique de propriétés numériques en présence de pointeurs

Fu, Zhoulai 22 July 2013 (has links)
Si la production de logiciel fiable est depuis longtemps la préoccupation d'ingénieurs, elle devient à ce jour une branche de sujets de recherche riche en applications, dont l'analyse statique. Ce travail a porté sur l'analyse statique de programmes et, plus précisément, sur l'analyse des propriétés numériques. Ces analyses sont traditionnellement basées sur le concept de domaine abstrait. Le problème est que, ce n'est pas évident d'étendre ces domaines dans le contexte de programmes avec pointeurs. Nous avons proposé une approche qui sait systématiquement combiner ces domaines avec l'information de l'analyse de points-to (une sorte d'analyse de pointeurs). L'approche est formalisée en théorie de l'interprétation abstraite, prouvée correct et prototypée avec une modular implémentation qui sait inférer des propriétés numériques des programmes de millions de lignes de codes. La deuxième partie de la thèse vise à améliorer la précision de l'analyse points-to. Nous avons découvert que l'analyse de must-alias (qui analyse si deux variables sont nécessairement égaux) peut servir à raffiner l'analyse points-to. Nous avons formalisé cette combinaison en s'appuyant sur la notion de bisimulation, bien connue en vérification de modèle ou théorie de jeu... Un algorithme de complexité quadruple est proposé et prouvé correct. / The fast and furious pace of change in computing technology has become an article of faith for many. The reliability of computer-based systems cru- cially depends on the correctness of its computing. Can man, who created the computer, be capable of preventing machine-made misfortune? The theory of static analysis strives to achieve this ambition. The analysis of numerical properties of programs has been an essential research topic for static analysis. These kinds of properties are commonly modeled and handled by the concept of numerical abstract domains. Unfor- tunately, lifting these domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have been intensively studied to an- alyze pointer behaviors and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. The static numerical anal- ysis is prototyped using the SOOT framework for pointer analyses and the PPL library for numerical domains. The implementation is able to analyze large Java program within several minutes. The second part of this thesis consists of a theoretical study of the com- bination of the points-to analysis with another pointer analysis providing information called must-alias. Two pointer variables must alias at some pro- gram control point if they hold equal reference whenever the control point is reached. We have developed an algorithm of quadruple complexity that sharpens points-to analysis using must-alias information. The algorithm is proved correct following a semantics-based formalization and the concept of bisimulation borrowed from the game theory, model checking etc.
35

Logico-Numerical Verification Methods for Discrete and Hybrid Systems / Méthodes logico-numériques pour la vérification des systèmes discrets et hybrides

Schrammel, Peter 18 October 2012 (has links)
Cette thèse étudie la vérification automatique de propriétés de sûreté de systèmes logico-numériques discrets ou hybrides. Ce sont des systèmes ayant des variables booléennes et numériques et des comportements discrets et continus. Notre approche est fondée sur l'analyse statique par interprétation abstraite. Nous adressons les problèmes suivants : les méthodes d'interprétation abstraite numériques exigent l'énumération des états booléens, et par conséquent, ils souffrent du probléme d'explosion d'espace d'états. En outre, il y a une perte de précision due à l'utilisation d'un opérateur d'élargissement afin de garantir la terminaison de l'analyse. Par ailleurs, nous voulons rendre les méthodes d'interprétation abstraite accessibles à des langages de simulation hybrides. Dans cette thèse, nous généralisons d'abord l'accélération abstraite, une méthode qui améliore la précision des invariants numériques inférés. Ensuite, nous montrons comment étendre l'accélération abstraite et l'itération de max-stratégies à des programmes logico-numériques, ce qui aide à améliorer le compromis entre l'efficacité et la précision. En ce qui concerne les systèmes hybrides, nous traduisons le langage de programmation synchrone et hybride Zelus vers les automates hybrides logico-numériques, et nous étendons les méthodes d'analyse logico-numérique aux systèmes hybrides. Enfin, nous avons mis en oeuvre les méthodes proposées dans un outil nommé ReaVer et nous fournissons des résultats expérimentaux. En conclusion, cette thèse propose une approche unifiée à la vérification de systèmes logico-numériques discrets et hybrides fondée sur l'interprétation abstraite qui est capable d'intégrer des méthodes d'interprétation abstraite numériques sophistiquées tout en améliorant le compromis entre l'efficacité et la précision. / This thesis studies the automatic verification of safety properties of logico-numerical discrete and hybrid systems. These systems have Boolean and numerical variables and exhibit discrete and continuous behavior. Our approach is based on static analysis using abstract interpretation. We address the following issues: Numerical abstract interpretation methods require the enumeration of the Boolean states, and hence, they suffer from the state space explosion problem. Moreover, there is a precision loss due to widening operators used to guarantee termination of the analysis. Furthermore, we want to make abstract interpretation-based analysis methods accessible to simulation languages for hybrid systems. In this thesis, we first generalize abstract acceleration, a method that improves the precision of the inferred numerical invariants. Then, we show how to extend abstract acceleration and max-strategy iteration to logico-numerical programs while improving the trade-off between efficiency and precision. Concerning hybrid systems, we translate the Zelus hybrid synchronous programming language to logico-numerical hybrid automata and extend logico-numerical analysis methods to hybrid systems. Finally, we implemented the proposed methods in ReaVer, a REActive System VERification tool, and provide experimental results. Concluding, this thesis proposes a unified approach to the verification of discrete and hybrid logico-numerical systems based on abstract interpretation, which is capable of integrating sophisticated numerical abstract interpretation methods while successfully trading precision for efficiency.
36

Constraint modelling and solving of some verification problems / Modélisation et résolution par contraintes de problèmes de vérification

Bart, Anicet 17 October 2017 (has links)
La programmation par contraintes offre des langages et des outils permettant de résoudre des problèmes à forte combinatoire et à la complexité élevée tels que ceux qui existent en vérification de programmes. Dans cette thèse nous résolvons deux familles de problèmes de la vérification de programmes. Dans chaque cas de figure nous commençons par une étude formelle du problème avant de proposer des modèles en contraintes puis de réaliser des expérimentations. La première contribution concerne un langage réactif synchrone représentable par une algèbre de diagramme de blocs. Les programmes utilisent des flux infinis et modélisent des systèmes temps réel. Nous proposons un modèle en contraintes muni d’une nouvelle contrainte globale ainsi que ses algorithmes de filtrage inspirés de l’interprétation abstraite. Cette contrainte permet de calculer des sur-approximations des valeurs des flux des diagrammes de blocs. Nous évaluons notre processus de vérification sur le langage FAUST, qui est un langage dédié à la génération de flux audio. La seconde contribution concerne les systèmes probabilistes représentés par des chaînes de Markov à intervalles paramétrés, un formalisme de spécification qui étend les chaînes de Markov. Nous proposons des modèles en contraintes pour vérifier des propriétés qualitatives et quantitatives. Nos modèles dans le cas qualitatif améliorent l’état de l’art tandis que ceux dans le cas quantitatif sont les premiers proposés à ce jour. Nous avons implémenté nos modèles en contraintes en problèmes de programmation linéaire en nombres entiers et en problèmes de satisfaction modulo des théories. Les expériences sont réalisées à partir d’un jeu d’essais de la bibliothèque PRISM. / Constraint programming offers efficient languages andtools for solving combinatorial and computationally hard problems such as the ones proposed in program verification. In this thesis, we tackle two families of program verification problems using constraint programming.In both contexts, we first propose a formal evaluation of our contributions before realizing some experiments.The first contribution is about a synchronous reactive language, represented by a block-diagram algebra. Such programs operate on infinite streams and model real-time processes. We propose a constraint model together with a new global constraint. Our new filtering algorithm is inspired from Abstract Interpretation. It computes over-approximations of the infinite stream values computed by the block-diagrams. We evaluated our verification process on the FAUST language (a language for processing real-time audio streams) and we tested it on examples from the FAUST standard library. The second contribution considers probabilistic processes represented by Parametric Interval Markov Chains, a specification formalism that extends Markov Chains. We propose constraint models for checking qualitative and quantitative reachability properties. Our models for the qualitative case improve the state of the art models, while for the quantitative case our models are the first ones. We implemented and evaluated our verification constraint models as mixed integer linear programs and satisfiability modulo theory programs. Experiments have been realized on a PRISM based benchmark.
37

Analyse statique de systèmes de contrôle commande : synthèse d'invariants non linéaires / Static Analysis of Control Command Systems : Synthesizing non Linear Invariants

Roux, Pierre 18 December 2013 (has links)
Les systèmes critiques comme les commandes de vol peuvent entraîner des désastres en cas de dysfonctionnement. D'où l'intérêt porté à la fois par le monde industriel et académique aux méthodes de preuve formelle capable d'apporter, plus ou moins automatiquement, une preuve mathématique de correction. Parmi elles, cette thèse s'intéresse particulièrement à l'interprétation abstraite, une méthode efficacepour générer automatiquement des preuves de propriétés numériques qui sont essentielles dans notre contexte.Il est bien connu des automaticiens que les contrôleurs linéaires sont stables si et seulement si ils admettent un invariant quadratique(un ellipsoïde, d'un point de vue géométrique). Ils les appellent fonction de Lyapunov quadratique et une première partie propose d'encalculer automatiquement pour des contrôleurs donnés comme paire de matrices. Ceci est réalisé en utilisant des outils de programmation semi-définie. Les aspects virgule flottante sont pris en compte, que ce soit dans les calculs effectués par le programme analysé ou dans les outils utilisés pour l'analyse. Toutefois, le véritable but est d'analyser des programmes implémentant des contrôleurs (et non des paires de matrices), incluant éventuellement des réinitialisation ou des saturations, donc non purement linéaires. L'itération sur les stratégies est une techniqued'analyse statique récemment développée et bien adaptée à nos besoins. Toutefois, elle ne se marrie pas facilement avec lestechniques classiques d'interprétation abstraite. La partie suivante propose une interface entre les deux mondes.Enfin, la dernière partie est un travail plus préliminaire sur l'usage de l'optimisation globale sur des polynômes basée sur les polynômes deBernstein pour calculer des invariants polynomiaux sur des programmes polynomiaux. / Critical Systems such as flight commands may have disastrous results in case of failure. Hence the interest of both the industrial and theacademic communities in formal methods able to more or less automatically deliver mathematical proof of correctness. Among them, this thesis will particularly focus on abstract interpretation, an efficient method to automatically generate proofs of numerical properties which are essential in our context.It is well known from control theorists that linear controllers are stable if and only if they admit a quadratic invariant (geometrically speaking, an ellipsoid). They call these invariants quadratic Lyapunov functions and a first part offers to automatically compute such invariants for controllers given as a pair of matrices. This is done using semi-definite programming optimization tools. It is worth noting that floating point aspects are taken care of, whether they affectcomputations performed by the analyzed program or by the tools used for the analysis.However, the actual goal is to analyze programs implementing controllers (and not pairs of matrices), potentially including resets or saturations, hence not purely linears. The policy iteration technique is a recently developed static analysis techniques well suited to that purpose. However, it does not marry very easily with the classic abstract interpretation paradigm. The next part tries to offer a nice interface between the two worlds.Finally, the last part is a more prospective work on the use of polynomial global optimization based on Bernstein polynomials to compute polynomial invariants on polynomials systems.
38

Collaboration de techniques formelles pour la vérification de propriétés de sûreté sur des systèmes de transition / Collaboration of formal techniques for the verification of safety properties over transition systems

Champion, Adrien 07 January 2014 (has links)
Ce travail porte sur la vérification de composants logiciels dans les systèmes embarqués critiques avioniques. Les conséquences d’une erreur dans de tels systèmes pouvant s'avérer catastrophiques, il se doivent de respecter leur spécification. La vérification formelle tend à prouver cette adéquation si elle est vraie, ou à produire un contre-exemple si elle ne l’est pas. Les méthodes actuelles ne sont pas capable de traiter les les systèmes industriels. La découverte d’informations supplémentaires (invariants) sur le système permet de réduire l’espace de recherche afin de renforcer l’objectif de preuve: les informations découvertes sont suffisantes pour conclure “facilement”. Nous définissons une architecture parallèle permettant à des méthodes de découverte d’invariants de collaborer autour d’un moteur de kinduction. Dans ce contexte nous proposons HullQe, une nouvelle heuristique de génération d’invariants potentiels combinant un calcul de pré-image par élimination de quantificateurs et des calculs d’enveloppes convexes. Nous montrons que HullQe est capable, automatiquement, de renforcer des objectifs de preuve correspondant à la vérification de patrons de conception courants en avionique. Pour autant que nous sachions, les méthodes actuelles sont incapables de conclure sur ces problèmes. Nous détaillons nos améliorations de l’algorithme d’élimination de quantificateurs de Monniaux afin d’assurer le passage à l’échelle sur nos systèmes. Notre framework formel Stuff est une implémentation de notre architecture parallèle composée de HullQe, d'une technique de découverte d’invariants basée sur des templates, et d'une généralisation de PDR à l’arithmétique. / This work studies the verification of software components in avionics critical embedded systems. As the failure of suchsystems can have catastrophic consequences, it is mandatory to make sure they are consistent with their specification.Formal verification consists in proving that a system respects its specification if it does, or to produce a counterexample if itdoes not. Current methods are unable to handle the verification problems stemming from realistic systems. Discoveringadditional information (invariants) on the system can however restrict the search space enough to strengthen the proofobjective: the information discovered allow to "easily" reach a conclusion. We define a parallel architecture for invariantdiscovery methods allowing them to collaborate around a k-induction engine. In this context we propose a new heuristic forthe generation of potential invariants by combining an iterated preimage calculus by quantifier elimination with convexhull computations, called HullQe. We show that HullQe is able to automatically strengthen proof objectives correspondingto safety properties on widespread design patterns in our field. To the best of our knowledge, these systems elude currenttechniques. We also detail our improvements to the quantifier elimination algorithm by David Monniaux in 2008, so that itscales to computing preimages on our systems. Our formal framework Stuff is an implementation of the parallel architecturewe propose in which we implemented not only HullQe, but also a template-based invariant discovery technique, and ageneralisation to Property Directed Reachability to linear real arithmetic and integer octagons.
39

Détermination de propriétés de flot de données pour améliorer les estimations de temps d'exécution pire-cas / Lookup of data flow properties to improve worst-case execution time estimations

Ruiz, Jordy 21 December 2017 (has links)
La recherche d'une borne supérieure au temps d'exécution d'un programme est une partie essentielle du processus de vérification de systèmes temps-réel critiques. Les programmes de tels systèmes ont généralement des temps d'exécution variables et il est difficile, voire impossible, de prédire l'ensemble de ces temps possibles. Au lieu de cela, il est préférable de rechercher une approximation du temps d'exécution pire-cas ou Worst-Case Execution Time (WCET). Une propriété cruciale de cette approximation est qu'elle doit être sûre, c'est-à-dire qu'elle doit être garantie de majorer le WCET. Parce que nous cherchons à prouver que le système en question se termine en un temps raisonnable, une surapproximation est le seul type d'approximation acceptable. La garantie de cette propriété de sûreté ne saurait raisonnablement se faire sans analyse statique, un résultat se basant sur une série de tests ne pouvant être sûr sans un traitement exhaustif des cas d'exécution. De plus, en l'absence de certification du processus de compilation (et de transfert des propriétés vers le binaire), l'extraction de propriétés doit se faire directement sur le code binaire pour garantir leur fiabilité. Toutefois, cette approximation a un coût : un pessimisme - écart entre le WCET estimé et le WCET réel - important entraîne des surcoûts superflus de matériel pour que le système respecte les contraintes temporelles qui lui sont imposées. Il s'agit donc ensuite, tout en maintenant la garantie de sécurité de l'estimation du WCET, d'améliorer sa précision en réduisant cet écart de telle sorte qu'il soit suffisamment faible pour ne pas entraîner des coûts supplémentaires démesurés. Un des principaux facteurs de surestimation est la prise en compte de chemins d'exécution sémantiquement impossibles, dits infaisables, dans le calcul du WCET. Ceci est dû à l'analyse par énumération implicite des chemins ou Implicit Path Enumeration Technique (IPET) qui raisonne sur un surensemble des chemins d'exécution. Lorsque le chemin d'exécution pire-cas ou Worst-Case Execution Path (WCEP), correspondant au WCET estimé, porte sur un chemin infaisable, la précision de cette estimation est négativement affectée. Afin de parer à cette perte de précision, cette thèse propose une technique de détection de chemins infaisables, permettant l'amélioration de la précision des analyses statiques (dont celles pour le WCET) en les informant de l'infaisabilité de certains chemins du programme. Cette information est passée sous la forme de propriétés de flot de données formatées dans un langage d'annotation portable, FFX, permettant la communication des résultats de notre analyse de chemins infaisables vers d'autres analyses. Les méthodes présentées dans cette thèse sont inclues dans le framework OTAWA, développé au sein de l'équipe TRACES à l'IRIT. Elles usent elles-mêmes d'approximations pour représenter les états possibles de la machine en différents points du programme. / The search for an upper bound of the execution time of a program is an essential part of the verification of real-time critical systems. The execution times of the programs of such systems generally vary a lot, and it is difficult, or impossible, to predict the range of the possible times. Instead, it is better to look for an approximation of the Worst-Case Execution Time (WCET). A crucial requirement of this estimate is that it must be safe, that is, it must be guaranteed above the real WCET. Because we are looking to prove that the system in question terminates reasonably quickly, an overapproximation is the only acceptable form of approximation. The guarantee of such a safety property could not sensibly be done without static analysis, as a result based on a battery of tests could not be safe without an exhaustive handling of test cases. Furthermore, in the absence of a certified compiler (and tech- nique for the safe transfer of properties to the binaries), the extraction of properties must be done directly on binary code to warrant their soundness. However, this approximation comes with a cost : an important pessimism, the gap between the estimated WCET and the real WCET, would lead to superfluous extra costs in hardware in order for the system to respect the imposed timing requirements. It is therefore important to improve the precision of the WCET by reducing this gap, while maintaining the safety property, as such that it is low enough to not lead to immoderate costs. A major cause of overestimation is the inclusion of semantically impossible paths, said infeasible paths, in the WCET computation. This is due to the use of the Implicit Path Enumeration Technique (IPET), which works on an superset of the possible execution paths. When the Worst-Case Execution Path (WCEP), corresponding to the estimated WCET, is infeasible, the precision of that estimation is negatively affected. In order to deal with this loss of precision, this thesis proposes an infeasible paths detection technique, enabling the improvement of the precision of static analyses (namely for WCET estimation) by notifying them of the infeasibility of some paths of the program. This information is then passed as data flow properties, formatted in the FFX portable annotation language, and allowing the communication of the results of our infeasible path analysis to other analyses.
40

Analyse de dépendances ML pour les évaluateurs de logiciels critiques. / ML Dependency Analysis for Critical-Software Assessors

Benayoun, Vincent 16 May 2014 (has links)
Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d’information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d’une définition formellede la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes. / Critical software needs to obtain an assessment before commissioning in order to ensure compliance tostandards. This assessment is given after a long task of software analysis performed by assessors. Theymay be helped by tools, used interactively, to build models using information-flow analysis. Tools likeSPARK-Ada exist for Ada subsets used for critical software. But some emergent languages such as thoseof the ML family lack such adapted tools. Providing similar tools for ML languages requires specialattention on specific features such as higher-order functions and pattern-matching. This work presentsan information-flow analysis for such a language specifically designed according to the needs of assessors.This analysis is built as an abstract interpretation of the operational semantics enriched with dependencyinformation. It is proved correct according to a formal definition of the notion of dependency using theCoq proof assistant. This work gives a strong theoretical basis for building an efficient tool for faulttolerance analysis.

Page generated in 0.1826 seconds