• 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.
21

Extensions des automates d'arbres pour la vérification de systèmes à états infinis

Murat, Valérie 26 June 2014 (has links) (PDF)
Les systèmes informatiques jouent un rôle essentiel dans la vie actuelle, et leurs erreurs peuvent avoir des conséquences dramatiques. Il existe des méthodes formelles permettant d'assurer qu'un système informatique est fiable. La méthode formelle utilisée dans cette thèse est appelée complétion d'automates d'arbres et permet d'analyser les systèmes à nombre d'états infini. Dans cette représentation, les états du système sont représentés par des termes et les ensembles d'états par des automates d'arbres. L'ensemble des comportements possibles d'un système est calculé grâce à l'application successive d'un système de réécriture modélisant le comportement du système vérifié. On garantit la fiabilité d'un système en vérifiant qu'un comportement interdit n'est pas présent dans l'ensemble des états accessibles. Mais cet ensemble n'est pas toujours calculable, et nous devons alors calculer une sur-approximation calculable de cet ensemble. Mais cette approximation peut s'avérer trop grossière et reconnaître de faux contre-exemples. La première contribution de cette thèse consiste alors à caractériser, par des formules logiques et de manière automatique, ce qu'est une "bonne" sur-approximation : une approximation représentant un sur-ensemble des configurations accessibles, et qui soit suffisamment précise pour ne pas reconnaître de faux contre-exemples. Résoudre ces formules conduit alors automatiquement à une sur-approximation concluante si elle existe, sans avoir recours à aucun paramétrage manuel. Le second problème de la complétion d'automates d'arbres est le passage à l'échelle, autrement dit le temps de calcul parfois élevé du calcul de complétion quand on s'attaque à des problèmes de la vie courante. Dans la vérification de programmes Java utilisant la complétion d'automates d'arbres, cette explosion peut être due à l'utilisation d'entiers de Peano. L'idée de notre seconde contribution est alors d'évaluer directement le résultat d'une opération arithmétique. D'une façon plus générale, il s'agit d'intégrer les éléments d'un domaine infini dans un automate d'arbres. En s'inspirant de méthodes issues de l'interprétation abstraite, cette thèse intègre des treillis abstraits dans les automates d'arbres, constituant alors un nouveau type d'automates. Les opérations sur le domaine infini représenté sont calculées en une seule étape d'évaluation plutôt que d'appliquer de nombreuses règles de réécriture. Nous avons alors adapté la complétion d'automates d'arbres à ce nouveau type d'automate, et la généricité du nouvel algorithme permet de brancher de nombreux treillis abstraits. Cette technique a été implémentée dans un outil appelé TimbukLTA, et cette implémentation permet de démontrer l'efficacité de cette technique.
22

Méthodes logico-numériques pour la vérification des systèmes discrets et hybrides

Schrammel, Peter 18 October 2012 (has links) (PDF)
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.
23

Extensions des automates d'arbres pour la vérification de systèmes à états infinis / Tree automata extensions for verification of infinite states systems

Murat, Valérie 26 June 2014 (has links)
Les systèmes informatiques jouent un rôle essentiel dans la vie actuelle, et leurs erreurs peuvent avoir des conséquences dramatiques. Il existe des méthodes formelles permettant d'assurer qu'un système informatique est fiable. La méthode formelle utilisée dans cette thèse est appelée complétion d'automates d'arbres et permet d'analyser les systèmes à nombre d'états infini. Dans cette représentation, les états du système sont représentés par des termes et les ensembles d'états par des automates d'arbres. L'ensemble des comportements possibles d'un système est calculé grâce à l'application successive d'un système de réécriture modélisant le comportement du système vérifié. On garantit la fiabilité d'un système en vérifiant qu'un comportement interdit n'est pas présent dans l'ensemble des états accessibles. Mais cet ensemble n'est pas toujours calculable, et nous devons alors calculer une sur-approximation calculable de cet ensemble. Mais cette approximation peut s'avérer trop grossière et reconnaître de faux contre-exemples. La première contribution de cette thèse consiste alors à caractériser, par des formules logiques et de manière automatique, ce qu'est une "bonne" sur-approximation : une approximation représentant un sur-ensemble des configurations accessibles, et qui soit suffisamment précise pour ne pas reconnaître de faux contre-exemples. Résoudre ces formules conduit alors automatiquement à une sur-approximation concluante si elle existe, sans avoir recours à aucun paramétrage manuel. Le second problème de la complétion d'automates d'arbres est le passage à l'échelle, autrement dit le temps de calcul parfois élevé du calcul de complétion quand on s'attaque à des problèmes de la vie courante. Dans la vérification de programmes Java utilisant la complétion d'automates d'arbres, cette explosion peut être due à l'utilisation d'entiers de Peano. L'idée de notre seconde contribution est alors d'évaluer directement le résultat d'une opération arithmétique. D'une façon plus générale, il s'agit d'intégrer les éléments d'un domaine infini dans un automate d'arbres. En s'inspirant de méthodes issues de l'interprétation abstraite, cette thèse intègre des treillis abstraits dans les automates d'arbres, constituant alors un nouveau type d'automates. Les opérations sur le domaine infini représenté sont calculées en une seule étape d'évaluation plutôt que d'appliquer de nombreuses règles de réécriture. Nous avons alors adapté la complétion d'automates d'arbres à ce nouveau type d'automate, et la généricité du nouvel algorithme permet de brancher de nombreux treillis abstraits. Cette technique a été implémentée dans un outil appelé TimbukLTA, et cette implémentation permet de démontrer l'efficacité de cette technique. / Computer systems are more and more important in everyday life, and errors into those systems can make dramatic damages. There are formal methods which can assure reliability of a system. The formal method used in this thesis is called tree automata completion and allows to analyze infinite state systems. In this representation, states of a system are represented by a term and sets of states by tree automata. The set of all reachable behaviors (or states) of the system is computed thanks to successive applications of a term rewriting system which represents the behavior of the system. The reliability of the system is assured by checking that no forbidden state is reachable by the system. But the set of reachable states is not always computable and we need to compute an over-approximation of it. This over-approximation is not always fine enough and can recognize counter examples. The first contribution of this thesis consist in characterizing by logical formulae, in an automatic way, what is a good approximation: an over-approximation which does not contain any counter example. Solving these formulae leads automatically to a good over-approximation if such an approximation exists, without any manual setting. An other problem of tree automata completion is the scaling when dealing with real life problems. In verification of Java programs using tree automata completion, this explosion may be due to the use of Peano numbers. The idea of the second contribution of this thesis is to evaluate directly the result of an arithmetic operation. Generally speaking, we integrate elements of an infinite domain in a tree automaton. Based on abstract interpretation, this thesis allows to integrate abstract lattice in tree automata. Operations on infinite domain are computed in one step of evaluation instead of probably many application of rewrite rules. Thus we adapted tree automata completion to this new type of tree automata with lattice, and genericity of the new algorithm allows to integrate many types of lattices. This technique has been implemented in a tool named TimbukLTA, and this implementation shows the efficiency of the technique.
24

Nouvelle algorithmique pour le calcul polyédral via programmation linéaire paramétrique / New algorithmics for polyhedral calculus via parametric linear programming

Maréchal, Alexandre 11 December 2017 (has links)
Cette thèse présente la nouvelle implémentation de la Verified Polyhedra Library (VPL), une bibliothèque efficace de calcul polyédral.Elle fournit des opérateurs certifiés en Coq, s'appliquant sur des représentations en contraintes.La version précédente souffrait d'inefficacité lors d'opérateurs cruciaux, à savoir l'élimination de variables et l'enveloppe convexe.Dans ce document, je présente des améliorations importantes qui bénéficient à la modularité, la simplicité et au passage à l'échelle de la bibliothèque:le processus de certification est généralisé et simplifié;les conditions polynomiales sont maintenant traitées;Les calculs qui n'impliquent pas de certification sont effectués en flottant;de nouveaux algorithmes sont fournis pour la minimisation de représentation et la détection d'égalités implicites.D'un côté, l'implémentation d'un solveur de problèmes de Programmation Linéaire Paramétrique (PLP) a mené à une meilleure efficacité tant en nombre de contraintes que de générateurs.L'élimination de variables et l'enveloppe convexe sont tous deux encodés en problème PLP.Le PLP est un outil générique possédant de nombreuses applications, et qui permet d'éviter la génération de redondances grâce à l'utilisation d'une contrainte de normalisation.De plus, nous proposons de nouveaux opérateurs pour la gestion des contraintes polynomiales, l'un d'entre eux étant également encodé en tant que problème PLP.De l'autre, la certification de la bibliothèque a été grandement optimisée et simplifiée.La VPL suit un paradigme de vérification a posteriori, où les calculs non triviaux sont effectués par des oracles externes générant des témoins de correction.Ces témoins sont ensuite validés par un vérifieur écrit en Coq.Grâce à un cadre de certification puissant et innovant, le Polymorphic Factory Style (PFS), la plupart des aspects délicats de la génération de témoins sont maintenant évitée.La souplesse du PFS est démontrée par la création d'une tactique en COQ qui découvre les égalités implicites en arithmétique linéaire. / This thesis presents the design and implementation of the Verified Polyhedra Library (VPL), a scalable library for polyhedral calculus.It provides Coq-certified polyhedral operators that work on constraints-only representation.The previous version was inefficient on crucial operations, namely variable elimination and convex hull.In this work, I present major improvements that have been made in scalability, modularity and simplicity:The certification process is generalized and simplified;Polynomial guards can now be handled;Computations that do not involve certification use floating-points;New algorithms are presented for minimization and detection of implicit equalities.On the one hand, the implementation of a solver for Parametric Linear Programming (PLP) problems led to an improved scalability both in dimension and in number of constraints.Variable elimination and convex hull are now encoded as such.PLP is a generic tool that has many applications, and that avoids generating redundancies thanks to a normalization constraint.Additionally, we provide new operators for handling multivariate polynomials, one of which being also encoded as a PLP problem.On the other hand, the certification part of the library has been greatly optimized and simplified.The VPL follows a result-verification paradigm, where complex computations are performed by untrusted oracles that generate witnesses of correctness, themselves validated by a certified Coq checker.Thanks to an innovative and powerful certification framework known as Polymorphic Factory Style (PFS), most cumbersome parts of the witness generation are now avoided.The flexibility of PFS is attested by the creation of a Coq tactic for learning equalities in linear arithmetic.
25

Binary level static analysis / Analyse statique au niveau binaire

Djoudi, Adel 02 December 2016 (has links)
Les méthodes de vérification automatique des logiciels connaissent un succès croissant depuis le début des années 2000, suite à plusieurs succès industriels (Microsoft, Airbus, etc.). L'analyse statique vise, à partir d'une description du programme, à inférer automatiquement des propriétés vérifiées par celui-ci. Les techniques standards d'analyse statique travaillent sur le code source du logiciel, écrit par exemple en C ou Java. Cependant, avoir accès au code source n'est pas envisageable pour de nombreuses applications relatives à la sécurité, soit que le code source n'est pas disponible (code mobile, virus informatiques), soit que le développeur ne veut pas le divulguer (composants sur étagère, certification par un tiers).Nous nous intéressons dans cette thèse à la conception et au développement d'une plate-forme d'analyse statique de code binaire à des fins d'analyse de sécurité. Nos principales contributions se font à trois niveaux: sémantique, implémentation et analyse statique.Tout d'abord, la sémantique des programmes binaires analysés est basée sur un formalisme générique appelé DBA qui a été enrichi avec des mécanismes de spécification et d'abstraction. La définition de la sémantique des programmes binaires requiert aussi un modèle mémoire adéquat.Nous proposons un modèle mémoire adapté au binaire, inspiré des travaux récents sur le code C bas-niveau. Ce nouveau modèle permet de profiter de l'abstraction du modèle à régions tout en gardant l'expressivité du modèle plat.Ensuite, notre plate-forme d'analyse de code binaire nommée BinSec offre trois services de base: désassemblage, simulation et analyse statique.Chaque instruction machine est traduite vers un bloc d'instructions DBA avec une sémantique équivalente. Une large partie des instructions x86 est gérée par la plateforme. Une passe de simplification permet d'éliminer les calculs intermédiaires inutiles afin d'optimiser le fonctionnement des analyses ultérieures. Nos simplifications permettent notamment d'éliminer jusqu'à75% des mises à jours de flags.Enfin, nous avons développé un moteur d'analyse statique de programmes binaires basé sur l'interprétation abstraite. Outre des domaines adaptés aux spécificités du code binaire, nous nous sommes concentrés sur le contrôle par l'utilisateur du compromis entre précision/correction et efficacité. De plus, nous proposons une approche originale de reconstruction de conditions dehaut-niveau à partir des conditions bas-niveau afin de gagner plus de précision d'analyse. L'approche est sûre, efficace, indépendante de la plateforme cibleet peut atteindre des taux de reconstruction très élevés. / Automatic software verification methods have seen increasing success since the early 2000s, thanks to several industrial successes (Microsoft, Airbus, etc.).Static program analysis aims to automatically infer verified properties of programs, based on their descriptions. The standard static analysis techniques apply on the software source code, written for instance in C or Java. However, access to source code is not possible for many safety-related applications, whether the source code is not available (mobile code, computer virus), or the developer does not disclose it (shelf components, third party certification).We are interested in this dissertation in design and development of a static binary analysis platform for safety analysis. Our contributions are made at three levels: semantics, implementation and static analysis.First, the semantics of analyzed binary programs is based on a generic, simple and concise formalism called DBA. It is extended with some specification and abstraction mechanisms in this dissertation. A well defined semantics of binary programs requires also an adequate memory model. We propose a new memory model adapted to binary level requirements and inspired from recent work on low-level C. This new model allows to enjoy the abstraction of the region-based memory model while keeping the expressiveness of the flat model.Second, our binary code analysis platform BinSec offers three basic services:disassembly, simulation and static analysis. Each machine instruction is translated into a block of semantically equivalent DBA instructions. The platform handles a large part of x86 instructions. A simplification step eliminates useless intermediate calculations in order to ease further analyses. Our simplifications especially allow to eliminate up to 75% of flag updates.Finally, we developed a static analysis engine for binary programs based on abstract interpretation. Besides abstract domains specifically adapted to binary analysis, we focused on the user control of trade offs between accuracy/correctness and efficiency. In addition, we offer an original approach for high-level conditions recovery from low-level conditions in order to enhance analysis precision. The approach is sound, efficient, platform-independent and it achieves very high ratio of recovery.
26

Static analysis on numeric and structural properties of array contents / Analyse statique des propriétés numériques et structurelles du tableau

Liu, Jiangchao 20 February 2018 (has links)
Dans cette thèse, nous étudions l'analyse statique par interprétation abstraites de programmes manipulant des tableaux, afin d'inférer des propriétés sur les valeurs numériques et les structures de données qui y sont stockées. Les tableaux sont omniprésents dans de nombreux programmes, et les erreurs liées à leur manipulation sont difficile à éviter en pratique. De nombreux travaux de recherche ont été consacrés à la vérification de tels programmes. Les travaux existants s'intéressent plus particulièrement aux propriétés concernant les valeurs numériques stockées dans les tableaux. Toutefois, les programmes bas-niveau (comme les systèmes embarqués ou les systèmes d'exploitation temps réel) utilisent souvent des tableaux afin d'y stocker des structures de données telles que des listes, de manière à éviter d'avoir recours à l'allocation de mémoire dynamique. Dans cette thèse, nous présentons des techniques permettant de vérifier par interprétation abstraite des propriétés concernant à la fois les données numériques ainsi que les structures composites stockées dans des tableaux. Notre première contribution est une abstraction qui permet de décrire des stores à valeurs numériques et avec valeurs optionnelles (i.e., lorsqu'une variable peut soit avoir une valeur numérique, soit ne pas avoir de valeur du tout), ou bien avec valeurs ensemblistes (i.e., lorsqu'une variable est associée à un ensemble de valeurs qui peut être vide ou non). Cette abstraction peut être utilisée pour décrire des stores où certaines variables ont un type option, ou bien un type ensembliste. Elle peut aussi servir à la construction de domaines abstraits pour décrire des propriétés complexes à l'aide de variables symboliques, par exemple, pour résumer le contenu de zones dans des tableaux. Notre seconde contribution est un domaine abstrait pour la description de tableaux, qui utilise des propriétés sémantiques des valeurs contenues afin de partitionner les cellules de tableaux en groupes homogènes. Ainsi, des cellules contenant des valeurs similaires sont décrites par les mêmes prédicats abstraits. De plus, au contraire des analyses de tableaux conventionnelles, les groupes ainsi formés ne sont pas nécessairement contigüs, ce qui contribue à la généralité de l'analyse. Notre analyse peut regrouper des cellules non-congitües, lorsque celles-ci ont des propriétés similaires. Ce domaine abstrait permet de construire des analyses complètement automatiques et capables d'inférer des invariants complexes sur les tableaux. Notre troisième contribution repose sur une combinaison de cette abstraction des tableaux avec différents domaines abstraits issus de l'analyse de forme des structures de données et reposant sur la logique de séparation. Cette combinaison appelée coalescence opère localement, et relie des résumés pour des structures dynamiques à des groupes de cellules du tableau. La coalescence permet de définir de manière locale des algorithmes d'analyse statique dans le domaine combiné. Nous l'utilisons pour relier notre domaine abstrait pour tableaux et une analyse de forme générique, dont la tâche est de décrire des structures chaînées. L'analyse ainsi obtenue peut vérifier à la fois des propriétés de sûreté et des propriétés de correction fonctionnelle. De nombreux programmes bas-niveau stockent des structures dynamiques chaînées dans des tableaux afin de n'utiliser que des zones mémoire allouées statiquement. La vérification de tels programmes est difficile, puisqu'elle nécessite à la fois de raisonner sur les tableaux et sur les structures chaînées. Nous construisons une analyse statique reposant sur ces trois contributions, et permettant d'analyser avec succés de tels programmes. Nous présentons des résultats d'analyse permettant la vérification de composants de systèmes d'exploitation et pilotes de périphériques. / We study the static analysis on both numeric and structural properties of array contents in the framework of abstract interpretation. Since arrays are ubiquitous in most software systems, and software defects related to mis-uses of arrays are hard to avoid in practice, a lot of efforts have been devoted to ensuring the correctness of programs manipulating arrays. Current verification of these programs by static analysis focuses on numeric content properties. However, in some lowlevel programs (like embedded systems or real-time operating systems), arrays often contain structural data (e.g., lists) without using dynamic allocation. In this manuscript, we present a series of techniques to verify both numeric and structural properties of array contents. Our first technique is used to describe properties of numerical stores with optional values (i.e., where some variables may have no value) or sets of values (i.e., where some variables may store a possibly empty set of values). Our approach lifts numerical abstract domains based on common linear inequality into abstract domains describing stores with optional values and sets of values. This abstraction can be used in order to analyze languages with some form of option scalar type. It can also be applied to the construction of abstract domains to describe complex memory properties that introduce symbolic variables, e.g., in order to summarize unbounded memory blocks like in arrays. Our second technique is an abstract domain which utilizes semantic properties to split array cells into groups. Cells with similar properties will be packed into groups and abstracted together. Additionally, groups are not necessarily contiguous. Compared to conventional array partitioning analyses that split arrays into contiguous partitions to infer properties of sets of array cells. Our analysis can group together non-contiguous cells when they have similar properties. Our abstract domain can infer complex array invariants in a fully automatic way. The third technique is used to combine different shape domains. This combination locally ties summaries in both abstract domains and is called a coalesced abstraction. Coalescing allows to define efficient and precise static analysis algorithms in the combined domain. We utilize it to combine our array abstraction (i.e., our second technique) and a shape abstraction which captures linked structures with separation logicbased inductive predicates. The product domain can verify both safety and functional properties of programs manipulating arrays storing dynamically linked structures, such as lists. Storing dynamic structures in arrays is a programming pattern commonly used in low-level systems, so as to avoid relying on dynamic allocation. The verification of such programs is very challenging as it requires reasoning both about the array structure with numeric indexes and about the linked structures stored in the array. Combining the three techniques that we have proposed, we can build an automatic static analysis for the verification of programs manipulating arrays storing linked structures. We report on the successful verification of several operating system kernel components and drivers.
27

Analyse et détection dynamique de codes viraux dans un contexte cryptographique

Josse, Sébastien 10 April 2009 (has links) (PDF)
Cette thèse est consacrée à la problématique de l'évaluation des produits antivirus. L'utilisateur final d'un produit antivirus ne sait pas toujours quelle confiance il peut placer dans son produit antivirus pour parer convenablement la menace virale. Pour répondre à cette question, il est nécessaire de formuler la problématique de sécurité à laquelle doit répondre un tel produit et de disposer d'outils et de critères méthodologiques, techniques et théoriques permettant d'évaluer la robustesse des fonctions de sécurité et la pertinence des choix de conception au regard d'une menace virale identifiée. Je concentre mon analyse de la menace virale sur quelques mécanismes (mécanismes cryptographiques, transformations de programme) adaptés au contexte boîte blanche, i.e. permettant à un virus de protéger ses données critiques en confidentialité et de masquer son fonctionnement dans un environnement complètement maîtrisé par l'attaquant. Une première étape incontournable avant toute organisation d'une ligne de défense consiste à analyser les virus, afin d'en comprendre le fonctionnement et les effets sur le système. Les méthodes et techniques de la rétro-ingénierie logicielle occupent ici - au côté des techniques de cryptanalyse - une place centrale. J'ai pris le parti de focaliser sur les méthodes dynamiques d'extraction d'information fondées sur une émulation du matériel supportant le système d'exploitation. L'évaluation d'un moteur de détection selon des critères objectifs requiert un effort de modélisation. J'étudie quelques modèles utilisés actuellement (grammaires formelles, interprétation abstraite, statistique). Chacun de ces modèles permet de formaliser certains aspects du problème de la détection virale. Je m'attache à l'étude des critères qu'il est possible de définir dans chacun de ces cadres formels et à leur utilisation pour partie des travaux d'évaluation d'un moteur de détection. Mes travaux m'ont conduit à la mise en oeuvre d'une approche méthodologique et d'une plate-forme de tests pour l'analyse de robustesse des fonctions et mécanismes d'un produit anti-virus. J'ai développé un outil d'analyse de code viral, appelé VxStripper, dont les fonctionnalités sont utiles à la réalisation de plusieurs des tests. Les outils formels sont utilisés pour qualifier en boîte blanche - ou sur la base des documents de conception détaillée - la conformité et l'efficacité d'un moteur de détection.
28

Domaines numériques abstraits faiblement relationnels

Miné, Antoine 06 December 2004 (has links) (PDF)
Le sujet de cette thèse est le développement de méthodes pour l'analyse automatique des programmes informatiques. Une des applications majeures est la conception d'outils pour découvrir les erreurs de programmations avant qu'elles ne se produisent, ce qui est crucial à l'heure où des tâches critiques mais complexes sont confiées à des ordinateurs. Nous nous plaçons dans le cadre de l'interprétation abstraite, qui est une théorie de l'approximation sûre des sémantiques de programmes, et nous nous intéressons en particulier aux domaines abstraits numériques spécialisés dans la découverte automatique des propriétés des variables numérique d'un programme.<br />Dans cette thèse, nous introduisons plusieurs nouveaux domaines numériques abstraits et en particulier le domaine des zones (permettant de découvrir des invariants de la forme X-Y≤c, des zones de congruence (X≡Y+c [b]) et des octogones (±X ±Y≤c). Ces domaines sont basés sur les concepts existants de graphe de potentiel, de matrice de différences bornées et sur l'algorithmique des plus courts chemins. Ils sont intermédiaires, en terme de précision et de coût, entre les domaines non relationnels (tel celui des intervalles), très peu précis, et les domaines relationnels classiques (tel celui des polyèdres), très coûteux. Nous les nommons " faiblement relationnels ". Nous présentons également des méthodes permettant d'appliquer les domaines relationnels à l'analyse de nombres à virgule flottante, jusqu'à présent uniquement réalisable par des domaines non relationnels donc peu précis. Enfin, nous présentons des méthodes génériques dites de " linéarisation " et de " propagation de constantes symboliques " permettant d'améliorer la précision de tout domaine numérique, pour un surcoût réduit.<br />Les méthodes introduites dans cette thèse ont été intégrées à Astrée, un analyseur spécialisé dans la vérification de logiciels embarqués critiques et se sont révélées indispensables pour prouver l'absence d'erreurs à l'exécution de logiciels de commande de vol électrique. Ces résultats expérimentaux viennent justifier l'intérêt de nos méthodes pour des cadre d'applications réelles.
29

Vérification de descriptions VHDL par interprétation abstraite.

Hymans, Charles 04 September 2004 (has links) (PDF)
Cette thèse traite de la vérification automatique de composants matériels décrits en VHDL. C'est une étude de faisabilité d'un outil de vérification automatique qui réunit: exhaustivité, efficacité de calcul et simplicité d'utilisation. La méthodologie de l'interprétation abstraite a été adoptée: l'algorithme de simulation de VHDL est d'abord formalisé par une sémantique opérationnelle, de laquelle une analyse statique est dérivée de façon systématique par abstraction. L'analyse calcule un sur-ensemble des états accessibles. Le domaine numérique utilisé pour représenter les valeurs possibles des signaux de la description peut être choisi librement. Une instance possible de l'analyse a été implémenté en OCaml. Le domaine numérique choisi ici est celui des égalités linéaires entre variables booléennes. L'outil a permi de valider un code correcteur d'erreur de type Reed Solomon. Les performances sont excellentes, en particulier meilleures que celles du model checker à base de BDDs VIS.
30

Analyse statique de manipulations de mémoire par interprétation abstraite -- Algorithmique des polyèdres tropicaux, et application à l'interprétation abstraite

Allamigeon, Xavier 30 November 2009 (has links) (PDF)
No description available.

Page generated in 0.2113 seconds