Le sujet central de cette thèse est le développement d'une méthode dédiée à la preuve de structures de données sans verrou. La motivation première vient du constat que les programmes concurrents sont devenu monnaie courante. Ceci a été possible par l'apparition de nouvelles primitives de synchronisation dans les nouvelles architectures matérielles. La seconde motivation est la quête de logiciel prouvé et donc correct. La sûreté des logiciels est en effet devenue primordiale de par la diffusion des systèmes embarqués et enfouis. La méthode proposée est basée sur le raffinement et dédiée à la conception et la vérification d'algorithme non-bloquant, en particulier ceux sans verrou. La méthode a été formalisée et sa correction prouvée en Isabelle/HOL. Un outil a par ailleurs été développé afin de générer des obligations de preuves à destination des solveurs SMT et des prouveurs de théorèmes du premier ordre. Nous l'avons utilisé afin de vérifier certains de ces algorithmes. / The central topic of this thesis is the proof-based development of lock-free data-structure algorithms. First motivation comes from new computer architectures that come with new synchronisation features. Those features enable concurrent algorithms that do not use locks and are thus more efficient. The second motivation is the search for proved correct program. Nowadays embedded software are used everywhere included in systems where safety is central. We propose a refinement-based method for designing and verifying non-blocking, and in particular lock-free, implementations of data structures. The entire method has been formalised in Isabelle/HOL. An associated prototype tool generates verification conditions that can be solved by SMT solvers or automatic theorem provers for first-order logic, and we have used this approach to verify a number of such algorithms.

A cause de la complexité croissante des systèmes sur puce (SoC), la vérification devient un aspect très important : 70 - 80% du coût de conception est alloué à cette tâche. Plus de 60% des projets de développement d'ASIC doivent être repris à cause des erreurs fonctionnelles, environ 50% des erreurs de conception étant situées au niveau du module. Dans le monde industriel, la vérification est souvent synonyme de simulation - une méthode de vérification naturelle pour les concepteurs, mais qui ne garantit pas l'absence d'erreurs. Une alternative est fournie par la vérification formelle qui prouve mathématiquement qu'un circuit satisfait une spécification. Dans cette thèse, on s'intéresse aux méthodes déductives basées sur la démonstration de théorèmes. La démonstration de théorèmes permet de vérifier formellement des descriptions matérielles de haut niveau et des systèmes réguliers ou très complexes, car la taille de données n'a plus d'importance. Par contre la modélisation de la description matérielle se fait directement en logique, ce qui rend l'accès difficile pour les concepteurs. Notre travail a pour but de faciliter l'introduction des outils de démonstration de théorèmes dans le flot de conception. Nous proposons une méthode automatique de traduction d'un circuit VHDL vers un modèle sémantique basé sur des équations récurrentes par rapport au temps qui peut être l'entrée de tout outil de démonstration de théorèmes et nous définissons une approche de vérification adaptée au modèle. Afin de valider notre proposition, nous avons choisi le démonstrateur ACL2 pour vérifier une bibliothèque de circuits de cryptographie.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

L'information judiciaire a connu une évolution remarquable en droit camerounais.Phase autonome et diligentée par un juge d’instruction, elle fut dès 1972, soit près d'unedizaine d'années après l'accession à l'indépendance, confiée à un autre organe, le Ministèrepublic, afin de lutter contre la recrudescence du grand banditisme. Le souci du législateur étaitde mettre en place une procédure adaptée, qui répond efficacement au dysfonctionnement dusystème judiciaire. Malheureusement, la nouvelle organisation de cette institution a montréses limites, en raison de la violation flagrante des principes gouvernant la procédure pénale etconstitutionnellement protégés d'une part ; et d'autre part, de la violation des droits et libertésindividuelles. Avec la mise en oeuvre de l'information judiciaire par le Ministère public, il yavait plus à craindre pour la violation de ces droits et libertés, surtout que les objectifs de lamanifestation de la vérité et d'une bonne administration de la justice n'étaient pas toujoursatteints. Il était donc nécessaire qu'une réorganisation de l'information judiciaire soitenvisagée. Cela a été rendu possible avec l'institution du Code de Procédure Pénale.L'entrée en vigueur de ce texte a permis d'observer un grand bouleversement dans laconduite de l'information judiciaire, mais également dans l'organisation de cette phase de laprocédure pénale et la protection des droits des parties. Le législateur est revenu sur lesprincipes traditionnels de la procédure pénale, en consacrant entre autres les principes de laprésomption d'innocence et de la séparation des fonctions de poursuite et d'instruction. Enoutre, en tenant compte de son passé historique, duquel est née une dualité judiciaire, lelégislateur a procédé à une véritable harmonisation des procédures de droit romanogermaniqueet de Common Law, en offrant aux parties les garanties nécessaires à laprotection de leurs intérêts respectifs.Cependant, force est de constater que malgré la réforme, l'objectif visé n'est pas atteint,non seulement parce que tous les éléments nécessaires à sa réalisation n'ont pas été pris encompte, mais en plus, le texte comporte de nombreuses lacunes, auxquelles on doit ajouter ladifficulté des autorités judiciaires à respecter ses dispositions. Il est donc inévitable de songerà une énième réforme, afin que la recherche de la vérité qui gouverne cette phase de laprocédure pénale se fasse dans des conditions qui concilient la bonne administration de lajustice et la protection des droits des parties. / The judicial investigation knew a remarkable evolution in Cameroonian law. Phaseautonomous and led by investigating judge, it was from 1972, around a decade after theestablishment of independence, assigned to another organ, the Prosecution, to fight against theoutbreak of the organized crime. The concern of the legislator was to set up an adaptedprocedure, which answers effectively the dysfunction of the judicial system. Unfortunately,the new organization of this institution showed its limits, because of the blatant violation ofthe principles governing the criminal procedure and constitutionally protected on one hand,and on the other hand, of the violation of the rights and the individual freedoms. With theimplementation of the judicial information by the Prosecution, there was more to be afraid forthe violation of these rights and liberties, especially that the objectives of the demonstration ofthe truth and the good administration of the justice were not still reached. It was thusnecessary to consider a reorganization of the judicial investigation. It was made possible withthe institution of the Code of Criminal Procedure.The entry into force of this text allowed to observe a deep upheaval in the conduct ofthe judicial investigation, but also in the organization of this phase of the criminal procedureand the protection of the rights of the parties. The legislator returned on the traditionalprinciples of the criminal procedure, by dedicating among others, the principles of thepresumption of innocence and the separation of prosecution and investigation functions.Furthermore, by taking into account his historic past, from which arose a judicial duality, thelegislator has to proceed to a real harmonization of the procedures of Roman Germanic Lawand Common Law, by offering to the parties the necessary guarantees for the protection oftheir respective interests.However, we have to admit that in spite of the reform, the aimed objective is notreached, not only because all requirements for its implementation were not taken into account,but moreover, the text contains numerous gaps, to which we have to add the difficulty of thejudicial authorities to respect its provisions. It’s thus inevitable to think of an umpteenthreform, so that the quest of truth which governs this phase of the criminal procedure is madein conditions which reconcile the good administration of the justice and the protection of therights of the parties.

Des nombreuses applications de méthodes formelles se fondent sur les solveurs SMT pour valider automatiquement les conditions à vérifier et fournissent des certificats de leurs résultats. Nous visons à la fois à améliorer l'efficacité des solveurs SMT et à accroître leur fiabilité. Notre première contribution est un cadre uniforme pour le raisonnement avec des formules quantifiées dans les solveurs SMT, dans lequel généralement diverses techniques d'instanciation sont utilisées. Nous montrons que les principales techniques d'instanciation peuvent être jetées dans ce cadre. Le cadre repose sur le problème de l'E-ground (dis)unification. Nous présentons une procédure de décision pour résoudre ce problème en pratique: Fermeture de congruence avec variables libres (CCFV}). Nous mesurons l'impact de CCFV dans les solveurs SMT veriT et CVC4. Nous montrons que nos implémentations présentent des améliorations par rapport aux approches à la fine pointe de la technologie. Notre deuxième contribution est un cadre pour le traitement des formules tout en produisant des preuves détaillées. Les principaux composants de notre cadre de production de preuve sont un algorithme de récurrence contextuelle générique et un ensemble extensible de règles d'inférence. Avec des structures de données appropriées, la génération des preuves ne crée que des frais généraux linéaires et les vérifications peuvent être vérifiées en temps linéaire. Nous avons également mis en œuvre l'approche en veriT. Cela nous a permis de simplifier considérablement la base du code tout en augmentant le nombre de problèmes pour lesquels des preuves détaillées peuvent être produites / In many formal methods applications it is common to rely on SMT solvers to automatically discharge conditions that need to be checked and provide certificates of their results. In this thesis we aim both to improve their efficiency of and to increase their reliability. Our first contribution is a uniform framework for reasoning with quantified formulas in SMT solvers, in which generally various instantiation techniques are employed. We show that the major instantiation techniques can be all cast in this unifying framework. Its basis is the problem of E-ground (dis)unification, a variation of the classic rigid E-unification problem. We introduce a decision procedure to solve this problem in practice: Congruence Closure with Free Variables (CCFV). We measure the impact of optimizations and instantiation techniques based on CCFV in the SMT solvers veriT and CVC4, showing that our implementations exhibit improvements over state-of-the-art approaches in several benchmark libraries stemming from real world applications. Our second contribution is a framework for processing formulas while producing detailed proofs. The main components of our proof producing framework are a generic contextual recursion algorithm and an extensible set of inference rules. With suitable data structures, proof generation creates only a linear-time overhead, and proofs can be checked in linear time. We also implemented the approach in veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced

L'apprentissage des preuves mathématiques déductives est fondamental dans l'enseignement des mathématiques. Pourtant, la dernière enquête TIMSS (Trends in International Mathematics and Science Study) menée par l'IEA ("International Association for the Evaluation of Educational Achievement") en mars 2015, le niveau général des étudiants en mathématiques est en baisse et les étudiants éprouvent de plus en plus de difficultés pour comprendre et écrire les preuves mathématiques déductives.Pour aborder ce problème, plusieurs travaux en didactique des mathématiques utilisent l’apprentissage collaboratif en classe.L'apprentissage collaboratif consiste à regrouper des étudiants pour travailler ensemble dans le but d'atteindre un objectif commun. Il repose sur le débat et l'argumentation. Les étudiants s'engagent dans des discussions pour exprimer leurs points de vue sous forme d'arguments et de contre-arguments dans le but de résoudre un problème posé.L’argumentation utilisée dans ces approches est basée sur des discussions informelles qui permettent aux étudiants d'exprimer publiquement leurs déclarations et de les justifier pour construire des preuves déductives. Ces travaux ont montré que l’argumentation est une méthode efficace pour l’apprentissage des preuves mathématiques : (i) elle améliore la pensée critique et les compétences métacognitives telles que l'auto-surveillance et l'auto-évaluation (ii) augmente la motivation des étudiants par les interactions sociales et (iii) favorise l'apprentissage entre les étudiants. Du point de vuedes enseignants, certaines difficultés surgissent avec ces approches pour l'évaluation des preuves déductives. En particulier, l'évaluation des résultats, qui comprend non seulement la preuve finale mais aussi les étapes intermédiaires, les discussions, les conflits qui peuvent exister entre les étudiants durant le débat. En effet, cette évaluation introduit une charge de travail importante pour les enseignants.Dans cette thèse, nous proposons un système pour la construction et l'évaluation des preuves mathématiques déductives. Ce système a un double objectif : (i) permettre aux étudiants de construire des preuves mathématiques déductives à partir un débat argumentatif structuré (ii) aider les enseignants à évaluer ces preuves et toutes les étapes intermédiaires afin d'identifier les erreurs et les lacunes et de fournir un retour constructif aux étudiants.Le système offre aux étudiants un cadre structuré pour débattre durant la construction de la preuve en utilisant les cadres d'argumentation proposés en intelligente artificielle. Ces cadres d’argumentation sont utilisés aussi dans l’analyse du débat qui servira pour représenter le résultat sous différentes formes afin de faciliter l’évaluation aux enseignants. Dans un second temps, nous avons implanté et validé le système par une étude expérimentale pour évaluer son acceptabilité dans la construction collaborative des preuves déductives par les étudiants et dans l’évaluation de ces preuves par les enseignants. / Learning deductive proofs is fundamental for mathematics education. Yet, many students have difficulties to understand and write deductive mathematical proofs which has severe consequences for problem solving as highlighted by several studies. According to the recent study of TIMSS (Trends in International Mathematics and Science Study), the level of students in mathematics is falling. students have difficulties to understand mathematics and more precisely to build and structure mathematical proofs.To tackle this problem, several approaches in mathematical didactics have used a social approach in classrooms where students are engaged in a debate and use argumentation in order to build proofs.The term "argumentation" in this context refers to the use of informal discussions in classrooms to allow students to publicly express claims and justify them to build proofs for a given problem. The underlying hypotheses are that argumentation: (i) enhances critical thinking and meta-cognitive skills such as self monitoring and self assessment; (ii) increases student's motivation by social interactions; and (iii) allows learning among students. From instructors' point of view, some difficulties arise with these approaches for assessment. In fact, the evaluation of outcomes -- that includes not only the final proof but also all intermediary steps and aborted attempts -- introduces an important work overhead.In this thesis, we propose a system for constructing and evaluating deductive mathematical proofs. The system has a twofold objective: (i) allow students to build deductive mathematical proofs using structured argumentative debate; (ii) help the instructors to evaluate these proofs and assess all intermediary steps in order to identify misconceptions and provide a constructive feedback to students. The system provides students with a structured framework to debate during construction of proofs using the proposed argumentation frameworks in artificial intelligence. These argumentation frameworks are also used in the analysis of the debate which will be used to represent the result in different forms in order to facilitate the evaluation to the instructors. The system has been implemented and evaluated experimentally by students in the construction of deductive proofs and instructors in the evaluation of these proofs.

Cette thèse présente une nouvelle optimisation de l'interprétation fonctionnelle (dite "Dialectica") de Gödel pour l'extraction de programmes plus efficaces à partir de preuves arithmétiques et même analytiques (classiques). La version dite "légère" de Dialectica se combine aussi et encore plus facilement avec l'optimisation dite "monotone" de Kohlenbach sur l'interprétation fonctionnelle de Gödel pour l'extraction de majorants et marges plus efficaces à partir de preuves monotones (classiques). La Dialectica légère est obtenue par l'adaptation des quantificateurs "uniformes" (sans signification computationnelle) de Berger. En plus, sa présentation est faite dans le style de la Déduction Naturelle, comme amélioration de l'adaptation récente de Jørgensen s! ur la Dialectica originelle de Gödel. Un bon nombre d'exemples concrèts sont traités sur l'ordinateur par la nouvelle technique d'extraction de programmes. La comparaison en machine avec la technique de synthèse de programmes appelée "A-traduction raffinée" de Berger, Buchholz et Schwichtenberg montre une très bonne performance de la Dialectica légère. Cette dernière n'est dépassée que dans le cas du Lemme de Dickson. Nous développons aussi la théorie de la synthèse de programmes efficaces, de complexité calculatoire polynômiale en temps, par la nouvelle Dialectica légère (monotone). Dans ce but nous métissons deux structures préexistantes de Cook-Urquhart-Ferreira et respectivement Kohlenbach pour obtenir une "Analyse bornée par des polynômes en temps". Ici, le résultat théorique est prometteur mais des exemple! s pratiques restent encore à trouver pour montrer la diff! ére nce de cette structure par rapport à l'"Analyse bornée par un polynôme" de Kohlenbach.

Dans les affaires judiciaires, les juges confrontés à des questions d’ordre techniques en matière informatique, recourent à des experts qui mettent leur savoir-faire au service de la justice. Régulièrement mandatés par les tribunaux, ils ont pour mission d'éclairer le juge en apportant des éléments de preuve utiles à l'enquête.Ils recherchent dans les scellés informatiques les éléments relatifs aux faits incriminés en préservant l’intégrité des données et évitant toute altération des supports originaux. Les éléments de preuve ainsi recueillis sont analysés par l’expert qui déposera ses conclusions au magistrat sous forme d’un rapport d'expertise.les investigations techniques sont effectuées à l'aide des outils très sophistiqués qui permettent de prendre connaissance des informations présentes, effacées, cachées ou chiffrées dans les supports numériques examinés.Ce qui requiert une parfaite maîtrise du matériel déployé et une identification claire des bonnes pratiques de la discipline. Ce projet de recherches vise à mettre en exergue les défis techniques aux quels sont confrontés les experts, la complexité des outils utilisés dans le cadre des investigations techniques et l'importance de la mise en place des tests de validation qui permettent de connaître les capacités et limites de chaque outil. / In criminal cases, judges confronted with questions of technical order in computer technology, designate expert witnesses who put their expertise at the service of justice. Duly appointed by the courts, they help the judge by providing evidence relevant to the investigation.They search the suspect’s seized digital devices for elements of computer related crime, while preserving the integrity of the data and avoiding any alteration of the original media.The evidence thus collected is analyzed by a digital forensic expert who will document their findings to the judge in a report.Technical investigations are conducted by using powerful and sophisticated tools to find the current files and recover deleted, hidden or encrypted data from the digital media device examined.This requires perfect control of the utilized equipment and a clear identification of the methods used during the analysis. This research project aims to highlight the technical challenges which experts face, the complexity of digital forensic tools used for technical investigations, and the importance of their validation to understand the capabilities and limitations of each tool.

La modélisation et la spécification de systèmes distribués nécessitent une adaptation des modèles logiques utilisés pour leur représentation. Les notions<br />d'emplacements et de ressources jouent notamment un rôle centrale dans la représentation de ces systèmes.<br /><br />On propose tout d'abord à la proposition d'une première logique, la logique linéaire distribuée et mobile (DMLL) qui intègre les notions de distribution et de mobilité. On propose également une sémantique à la Kripke et un calcul des séquents supportant l'élimination des coupures pour cette logique.<br /><br />Cette première étude a mis en avant le rôle centrale de la sémantique pour la modélisation de systèmes distribués. On propose alors la structure des arbres de ressources, des arbres dont les noeuds possèdent des labels et contiennent des ressources appartenant à<br />monoïde partiel de ressources et BI-Loc, une logique pour raisonner sur ces arbres, un langage permettant de modifier les arbres et son axiomatisation correcte et complète sous forme de triplets de Hoare. Concernant BI-Loc, on détermine des conditions suffisantes pour décider de la satisfaction et de la validité par model-checking et on développe une méthode de preuves fondée sur les tableaux sémantiques correcte et complète.<br /><br />On montre comment on peut raisonner sur les tas de pointeurs grâce aux arbres de ressources. Enfin, on détermine comment le modèle des arbres partiel peut être utilisé pour représenter et spécifier les données<br />semi-structurées et raisonner sur la transformation de ce type de données.

L'objectif de cette thèse est de produire un environnement permettant de raisonner formellement sur la correction de systèmes de calculs locaux, ainsi que sur l'expressivité de ce modèle de calcul. Pour ce faire, nous utilisons l'assistant de preuve Coq. Notre première contribution est la formalisation en Coq de la sémantique des systèmes de réétiquetage localement engendrés, ou calculs locaux. Un système de calculs locaux est un système de réétiquetage de graphe dont la portée est limitée. Nous proposons donc tout d'abord une implantation succincte de la théorie des graphes en Coq, et utilisons cette dernière pour définir les systèmes de réétiquetage de graphes localement engendrés. Nous avons relevé, dans la définition usuelle des calculs locaux, certaines ambiguïtés. Nous proposons donc une nouvelle définition, et montrons formellement que celle-ci capture toutes les sous-classes d'algorithmes étudiées. Nous esquissons enfin une méthodologie de preuve des systèmes de calculs locaux en Coq.Notre seconde contribution consiste en l'étude formelle de l'expressivité des systèmes de calculs locaux. Nous formalisons un résultat de D. Angluin (repris par la suite par Y. Métivier et J. Chalopin): l'inexistence d'un algorithme d'élection universelle. Nous proposons ensuite deux lemmes originaux concernant les calculs locaux sur les arêtes (ou systèmes LC0), et utilisons ceux-ci pour produire des preuves formelles d'impossibilité pour plusieurs problèmes: calcul du degré de chaque sommet, calcul d'arbre recouvrant, etélection. Nous proposons informellement une nouvelles classes de graphe pour laquelle l'élection est irréalisable par des calculs locaux sur les arêtes.Nous étudions ensuite les transformations de systèmes de calculs locaux et de leur preuves. Nous adaptons le concept de Forward Simulation de N. Lynch aux systèmes de calculs locaux et utilisons ce dernier pour démontrer formellement l'inclusion de deux modes de détection de terminaison dans le cas des systèmes LC0. La preuve de cette inclusion estsimplifiée par l'utilisation de transformations "standards" de systèmes, pour lesquels des résultats génériques ont été démontrés. Finalement, nous réutilisons ces transformations standards pour étudier, en collaboration avec M. Tounsi, deux techniques de composition des systèmes de réétiquetage LC0. Une bibliothèque Coq d'environ 50000 lignes, contenant les preuves formelles des théorèmes présentés dans le mémoire de thèse à été produite en collaboration avec Pierre Castéran (dont environ 40%produit en propre par V. Filou) au cours de cette thèse. / The goal of this work is to build a framework allowing the study, in aformal setting, of the correctness of local computations systems aswell as the expressivity of this model. A local computation system isa set of graph relabelling rules with limited scope, corresponding to a class of distributed algorithms.Our first contribution is the formalisation, in the Coq proofassistant, of a relationnal semantic for local computation systems.This work is based on an original formal graph theory for Coq.Ambiguities inherent to a "pen and paper" definition of local computations are corrected, and we prove that our definition captures all sub-classes of relabelling relations studied in the remainder. We propose a draft of a proof methodology for local computation systems in Coq. Our second contribution is the study of the expressivity of classes of local computations inside our framework. We provide,for instance, a formal proof of D. Angluin results on election and graph coverings. We propose original "meta-theorems" concerningthe LC0 class of local computation, and use these theorem to produce formal impossibility proofs.Finally we study possible transformations of local computation systemsand of their proofs. To this end, we adapt the notion of ForwardSimulation, originally formulated by N. Lynch, to localcomputations. We use this notion to define certified transformationsof LC0 systems. We show how those certified transformation can be useto study the expressivity of certain class of algorithm in ourframework. We define, as certified transformation, two notions ofcomposition for LC0 systems.A Coq library of ~ 50000 lines of code, containing the formal proofs of the theorems presented in the thesis has been produced in collaboration with Pierre Castéran.