Les techniques de vérification déductive fournissent des méthodes puissantes pour la vérification formelle des propriétés exprimées dans la Logique de Hoare. Dans cette formalisation, également connue sous le nom de sémantique axiomatique, un programme est considéré comme un transformateur de prédicat, où chaque programme c exécuté sur un état vérifiant une propriété P conduit à un état vérifiant une autre propriété Q. Les propriétés relationnelles, de leur côté, lient un ensemble de programmes à deux propriétés. Plus précisément, une propriété relationnelle est une propriété concernant n programmes c1; ::::; cn, indiquant que si chaque programme ci commence dans un état si et termine dans un état s0 i tel que P(s1; ::::; sn) soit vérifié, alors Q(s0 1; :::; s0 n) est vérifié. Ainsi, les propriétés relationnelles invoquent tout nombre fini d’exécutions de programmes éventuellement dissemblables. De telles propriétés ne peuvent pas être exprimées directement dans le cadre traditionnel de la vérification déductive modulaire, car la sémantique axiomatique ne peut se référer à deux exécutions distinctes d’un programme c, ou à des programmes différents c1 et c2. Cette thèse apporte deux solutions à la vérification déductive des propriétés relationnelles. Les deux approches permettent de prouver une propriété relationnelle et de l’utiliser comme hypothèse dans des vérifications ultérieures. Nous modélisons ces solutions à l’aide d’un mini-langage impératif contenant des appels de procédures. Les deux solutions sont implémentées dans le contexte du langage de programmation C, de la plateforme FRAMA-C, du langage de spécification ACSL et du plugin de vérification déductive WP. Le nouvel outil, appelé RPP, permet de spécifier une propriété relationnelle, de la prouver en utilisant la vérification déductive classique, et de l’utiliser comme hypothèse dans la preuve d’autres propriétés. L’outil est évalué sur une série d’exemples illustratifs. Des expériences ont également été faites sur la vérification à l’exécution de propriétés relationnelles et la génération de contre-exemples lorsqu’une propriété ne peut être prouvée. / Deductive verification techniques provide powerful methods for formal verification of properties expressed in Hoare Logic. In this formalization, also known as axiomatic semantics, a program is seen as a predicate transformer, where each program c executed on a state verifying a property P leads to a state verifying another property Q. Relational properties, on the other hand, link n program to two properties. More precisely, a relational property is a property about n programs c1; :::; cn stating that if each program ci starts in a state si and ends in a state s0 i such that P(s1; :::; sn) holds, then Q(s0 1; :::; s0 n) holds. Thus, relational properties invoke any finite number of executions of possibly dissimilar programs. Such properties cannot be expressed directly in the traditional setting of modular deductive verification, as axiomatic semantics cannot refer to two distinct executions of a program c, or different programs c1 and c2. This thesis brings two solutions to the deductive verification of relational properties. Both of them make it possible to prove a relational property and to use it as a hypothesis in the subsequent verifications. We model our solutions using a small imperative language containing procedure calls. Both solutions are implemented in the context of the C programming language, the FRAMA-C platform, the ACSL specification language and the deductive verification plugin WP. The new tool, called RPP, allows one to specify a relational property, to prove it using classic deductive verification, and to use it as hypothesis in the proof of other properties. The tool is evaluated over a set of illustrative examples. Experiments have also been made on runtime checking of relational properties and counterexample generation when a property cannot be proved.

Vérifier formellement des programmes concurrents est une tâche difficile. S’il existe différentes techniques pour la réaliser, très peu sont effectivement mises en oeuvre pour des programmes écrits dans des langages de programmation réalistes. En revanche, les techniques de vérification formelles de programmes séquentiels sont utilisées avec succès depuis plusieurs années déjà, et permettent d’atteindre de hauts degrés de confiance dans nos systèmes. Cette thèse propose une alternative aux méthodes d’analyses dédiées à la vérification de programmes concurrents consistant à transformer le programme concurrent en un programme séquentiel pour le rendre analysable par des outils dédiés aux programmes séquentiels. Nous nous plaçons dans le contexte de FRAMA-C, une plate-forme d’analyse de code C spécifié avec le langage ACSL. Les différentes analyses de FRAMA-C sont des greffons à la plate-forme, ceux-ci sont à ce jour majoritairement dédiés aux programmes séquentiels. La méthode de vérification que nous proposons est appliquée manuellement à la vérification d’un code concurrent issu d’un hyperviseur. Nous automatisons la méthode à travers un nouveau greffon à FRAMA-C qui permet de produire automatiquement, depuis un programme concurrent spécifié, un programme séquentiel spécifié équivalent. Nous présentons les bases de sa formalisation, ayant pour but d’en prouver la validité. Cette validité n’est valable que pour la classe des programmes séquentiellement consistant. Nous proposons donc finalement un prototype de solveur de contraintes pour les modèles mémoire faibles, capable de déterminer si un programme appartient bien à cette classe en fonction du modèle mémoire cible. / Formal verification of concurrent programs is a hard task. There exists different methods to perform such a task, but very few are applied to the verification of programs written using real life programming languages. On the other side, formal verification of sequential programs is successfully applied for many years, and allows to get high confidence in our systems. As an alternative to dedicated concurrent program analyses, we propose a method to transform concurrent programs into sequential ones to make them analyzable by tools dedicated to sequential programs. This work takes place within the analysis framework FRAMA-C, dedicated to the analysis of C code specified with ACSL. The different analyses provided by FRAMA-C are plugins to the framework, which are currently mostly dedicated to sequential programs. We apply this method to the verification of a concurrent code taken from an hypervisor. We describe the automation of the method implemented by a new plugin to FRAMAC that allow to produce, from a specified concurrent program, an equivalent specified sequential program. We present the basis of a formalization of the method with the objective to prove its validity. This validity is admissible only for the class of sequentially consistent programs. So, we finally propose a prototype of constraint solver for weak memory models, which is able to determine whether a program is in this class or not, depending on the targeted hardware.

Le problème général de la preuve de propriétés de programmes impératifs est indécidable. Pour deslangages de programmation et de propriétés plus restrictifs, des sous-problèmes décidables sontconnus. En pratique, grâce à des heuristiques, les outils de preuve de programmes automatisent despreuves qui sortent du cadre théorique de ces sous-problèmes décidables connus. Nous illustronscette réussite pratique en construisant un catalogue de preuves, pour des programmes et despropriétés de nature similaire et de complexité croissante. Ces programmes sont principalementdes générateurs de cartes combinatoires.Ainsi, ce travail contribue aux domaines de recherche de la combinatoire énumérative et dugénie logiciel. Nous distribuons une bibliothèque C de générateurs exhaustifs bornés de tableauxstructurés, formellement spécifiés en ACSL et vérifiés avec le greffon WP de la plateforme d’analyseFrama-C. Nous proposons également une méthodologie de test qui facilite la preuve interactive enCoq, une étude formelle des cartes originale, et de nouveaux résultats en combinatoire énumérative. / The general problem of proving properties of imperative programs is undecidable. Some subproblems– restricting the languages of programs and properties – are known to be decidable. Inpractice, thanks to heuristics, program proving tools sometimes automate proofs for programs andproperties living outside of the theoretical framework of known decidability results. We illustrate thisfact by building a catalog of proofs, for similar programs and properties of increasing complexity. Mostof these programs are combinatorial map generators.Thus, this work contributes to the research fields of enumerative combinatorics and softwareengineering. We distribute a C library of bounded exhaustive generators of structured arrays, formallyspecified in ACSL and verified with the WP plugin of the Frama-C analysis platform. We also proposea testing-based methodology to assist interactive proof in Coq, an original formal study of maps, andnew results in enumerative combinatorics.

Sur des architectures récentes, un programme numérique peut donner des réponses différentes en fonction du hardware et du compilateur. Ces incohérences des résultats viennent du fait que chaque calcul en virgule flottante est effectué avec des précisions différentes. Le but de cette thèse est de prouver formellement des propriétés des programmes opérant sur des nombres flottants en prenant en compte l’architecture et le compilateur. Pour le faire, nous avons proposé deux approches différentes. La première approche est de prouver des propriétés des programmes en virgule flottante qui sont vraies sur plusieurs architectures et compilateurs. Cette approche ne considère que les erreurs d’arrondi qui doivent être validées quels que soient l’environnement matériel et le choix du compilateur. Elle est implantée dans la plate-forme Frama-C pour l’analyse statique de code C. La deuxième approche consiste à prouver des propriétés des programmes en analysant leur code assembleur. Nous nous concentrons sur des problèmes et des pièges qui apparaissent sur des calculs en virgule flottante. L’analyse directe du code assembleur nous permet de considérer des caratéristiques dépendant de l’architecture ou du compilateur telle que l’utilisation des registres en précision étendue. Cette approche est implantée comme une sur-couche de la plate-forme Why pour la vérification déductive. / On some recently developed architectures, a numerical program may give different answers depending on the execution hardware and the compilation. These discrepancies of the results come from the fact that each floating-point computation is calculated with different precisions. The goal of this thesis is to formally prove properties about numerical programs while taking the architecture and the compiler into account. In order to do that, we propose two different approaches. The first approach is to prove properties of floating-point programs that are true for multiple architectures and compilers. This approach states the rounding error of each floating-point computation whatever the environment and the compiler choices. It is implemented in the Frama-C platform for static analysis of C code. The second approach is to prove behavioral properties of numerical programs by analyzing their compiled assembly code. We focus on the issues and traps that may arise on floating-point computations. Direct analysis of the assembly code allows us to take into account architecture- or compiler-dependent features such as the possible use of extended precision registers. It is implemented above the Why platform for deductive verification

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-08-26T23:09:02Z No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-08-30T23:32:12Z (GMT) No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5) / Made available in DSpace on 2016-08-30T23:32:12Z (GMT). No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5) Previous issue date: 2016-04-29 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior (CAPES) / A presente disserta??o descreve uma extens?o para a plataforma Frama-C e o plugin WP:o WPTrans. Essa extens?o permite a manipula??o, atrav?s de regras de infer?ncia, dasobriga??es de prova geradas pelo WP, com a possibilidade das mesmas serem enviadas,em qualquer etapa da modifica??o, a solucionadores SMT e assistentes de prova. Algumasobriga??es de prova podem ser validadas automaticamente, enquanto outras s?o muitocomplexas para os solucionadores SMT, exigindo uma prova manual pelo desenvolvedor,atrav?s dos assistentes de prova. Contudo, a segunda abordagem geralmente requer dousu?rio uma experi?ncia significativa em estrat?gias de prova. Alguns assistentes oferecemcomunica??o com provadores autom?ticos, entretanto, esta liga??o pode ser complexaou incompleta, restando ao usu?rio apenas a prova manual. O objetivo deste plugin ? interligaros dois tipos de ferramentas de modo preciso e completo, com uma linguagemsimples para a manipula??o. Assim, o usu?rio pode simplificar suficientemente as obriga??es deprova para que possam ser validadas por qualquer outro solucionador SMT.N?o obstante, a extens?o ? interligada diretamente ao WP, facilitando a instala??o doplugin no Frama-C. Esta extens?o tamb?m ? uma porta de entrada para outras poss?veisfuncionalidades, sendo as mesmas discutidas neste documento. / The platform Frama-C is a tool dedicated to analysis of source code of software written in C, with the possible types of analysis provided by plugins attached to the platform. One of its plugins is WP, used for deductive veri cation of C code with ACSL, a formal speci cation language. This dissertation describes the extension of this plugin, named WPTrans. This extension allows generated proof obligations from WP to be manipulated through inference rules and sent, at any stage of the proof, to automatic (mainly SMT solvers) and interactive theorem provers. Some proof obligations may be proved automatically, while others can be too complex to be solved by automatic theorem provers, requiring the users of Frama-C and WP to handle them manually. This approach usually requires a signi cant experience in proof strategies. Some interactive theorem provers provide communication with automatic provers. However, this connection can be complex and incomplete, leaving the user with the manual proof option only. The strength of WPTrans is to combine the features of automatic and interactive theorem provers in a precise and complete way, with a simple manipulation language. Thus, the user can simplify the proof obligations enough in order for its proof to be concluded with an SMT solver, letting the proof be partially manual and partially automatic. Nevertheless, the plugin is directly linked do WP, facilitating the installation of the extension in Frama-C. This tool is also a gateway to other possible features, which we discuss herein.

La vérification de logiciels repose le plus souvent sur une spécification formelle encodant les propriétés du programme à vérifier. La tâche de spécification et de vérification déductive des programmes est longue et difficile et nécessite une connaissance des outils de preuve de programmes. En effet, un échec de preuve de programme peut être dû à une non-conformité du code par rapport à sa spécification, à un contrat de boucle ou de fonction appelée trop faible pour prouver une autre propriété, ou à une incapacité du prouveur. Il est souvent difficile pour l’utilisateur de décider laquelle de ces trois raisons est la cause de l’échec de la preuve car cette information n’est pas (ou rarement) donnée par le prouveur et requiert donc une revue approfondie du code et de la spécification. L’objectif de cette thèse est de fournir une méthode de diagnostic automatique des échecs de preuve afin d’améliorer le processus de spécification et de preuve des programmes C. Nous nous plaçons dans le cadre de la plate-forme d’analyse des programmes C FRAMA-C, qui fournit un langage de spécification unique ACSL, un greffon de vérification déductive WP et un générateur de tests structurels PATHCRAWLER. La méthode que nous proposons consiste à diagnostiquer les échecs de preuve en utilisant la génération de tests structurels sur une version instrumentée du programme d’origine / Software verification often relies on a formal specification encoding the program properties to check. Formally specifying and deductively verifying programs is difficult and time consuming and requires some knowledge about theorem provers. Indeed, a proof failure for a program can be due to a noncompliance between the code and its specification, a loop or callee contrat being insufficient to prove another property, or a prover incapacity. It is often difficult for the user to decide which one of these three reasons causes a given proof failure. Indeed, this feedback is not (or rarely) provided by the theorem prover thus requires a thorough review of the code and the specification. This thesis develops a method to automatically diagnose proof failures and facilitate the specification and verification task. This work takes place within the analysis framework for C programs FRAMAC, that provides the specification language ACSL, the deductive verification plugin WP, and the structural test generator PATHCRAWLER. The proposed method consists in diagnosing proof failures using structural test generation on an instrumented version of the program under verification.

On some recently developed architectures, a numerical program may give different answers depending on the execution hardware and the compilation. These discrepancies of the results come from the fact that each floating-point computation is calculated with different precisions. The goal of this thesis is to formally prove properties about numerical programs while taking the architecture and the compiler into account. In order to do that, we propose two different approaches. The first approach is to prove properties of floating-point programs that are true for multiple architectures and compilers. This approach states the rounding error of each floating-point computation whatever the environment and the compiler choices. It is implemented in the Frama-C platform for static analysis of C code. The second approach is to prove behavioral properties of numerical programs by analyzing their compiled assembly code. We focus on the issues and traps that may arise on floating-point computations. Direct analysis of the assembly code allows us to take into account architecture- or compiler-dependent features such as the possible use of extended precision registers. It is implemented above the Why platform for deductive verification