Ce mémoire présente l'implémentation d'un nouveau langage de programmation nommé Typer. Typer est un langage fonctionnel orienté vers la méta programmation. Il a été conçu pour augmenter la productivité du programmeur et lui permettre d'écrire des applications plus fiables grâce à son système de types. Pour arriver à ses fins, Typer utilise l'inférence de types et implémente un puissant système de macros. L'inférence de types permet à l'utilisateur d'omettre certains éléments, le système de macros, quant à lui, permet de compléter le programme pendant la compilation lorsque l'inférence n'est pas suffisante ou pour générer du code. Typer utilise les types dépendants pour permettre à l'utilisateur de créer des types très expressifs pouvant même être utilisés pour représenter des preuves formelles. De plus, l'expressivité des types dépendants permet au compilateur d'effectuer des vérifications plus approfondies pendant la compilation même. Ces mécaniques permettent au code source d'être moins verbeux, plus concis et plus simple à comprendre, rendant, ainsi l'écriture de programmes ou/et de preuves plus plaisante. Ces fonctionnalités sont implémentées dans l'étape que nous appelons l'élaboration, à l'intérieur de laquelle de nombreuses transformations du code source ont lieu. Ces transformations incluent l'élimination des aides syntaxiques, la résolution des identificateurs, l'expansion des macros, la propagation et l'inférence des types. / This dissertation present the implementation of a new programming language named Typer Typer is a functional programming language oriented towards meta programming. It has been created to increase the programmer productivity and enable him to write safer programs thanks to his type system. To achieve his goal, Typer use type inference and a powerful macro system. Type inference enable to user to elide some elements while the macro system enable us to complete the program during compilation. Typer use dependent type which enable the user to create very expressive types which can even be used to represent formal proofs. Furthermore, dependent type's expressivity enable the compiler to perform a in-depth checks during compilation. Those mechanics enable the source code to be less verbose, shorter and easier to understand, making the writing of new programmes more enjoyable. Those functionalities are implemented during the step we call the elaboration in which numerous transformations occur. Those transformations include the removal of syntactic sugar, identifier resolution, macro expansion and the propagation and the inference of types.

Cette thèse contient des preuves de convergence ou de divergence d'algorithmes d'optimisation appelés stratégies d'évolution (ESs), ainsi que le développement d'outils mathématiques permettant ces preuves.Les ESs sont des algorithmes d'optimisation stochastiques dits ``boîte noire'', i.e. où les informations sur la fonction optimisée se réduisent aux valeurs qu'elle associe à des points. En particulier, le gradient de la fonction est inconnu. Des preuves de convergence ou de divergence de ces algorithmes peuvent être obtenues via l'analyse de chaînes de Markov sous-jacentes à ces algorithmes. Les preuves de convergence et de divergence obtenues dans cette thèse permettent d'établir le comportement asymptotique des ESs dans le cadre de l'optimisation d'une fonction linéaire avec ou sans contrainte, qui est un cas clé pour des preuves de convergence d'ESs sur de larges classes de fonctions.Cette thèse présente tout d'abord une introduction aux chaînes de Markov puis un état de l'art sur les ESs et leur contexte parmi les algorithmes d'optimisation continue boîte noire, ainsi que les liens établis entre ESs et chaînes de Markov. Les contributions de cette thèse sont ensuite présentées:o Premièrement des outils mathématiques généraux applicables dans d'autres problèmes sont développés. L'utilisation de ces outils permet d'établir aisément certaines propriétés (à savoir l'irreducibilité, l'apériodicité et le fait que les compacts sont des small sets pour la chaîne de Markov) sur les chaînes de Markov étudiées. Sans ces outils, établir ces propriétés était un processus ad hoc et technique, pouvant se montrer très difficile.o Ensuite différents ESs sont analysés dans différents problèmes. Un (1,\lambda)-ES utilisant cumulative step-size adaptation est étudié dans le cadre de l'optimisation d'une fonction linéaire. Il est démontré que pour \lambda > 2 l'algorithme diverge log-linéairement, optimisant la fonction avec succès. La vitesse de divergence de l'algorithme est donnée explicitement, ce qui peut être utilisé pour calculer une valeur optimale pour \lambda dans le cadre de la fonction linéaire. De plus, la variance du step-size de l'algorithme est calculée, ce qui permet de déduire une condition sur l'adaptation du paramètre de cumulation avec la dimension du problème afin d'obtenir une stabilité de l'algorithme. Ensuite, un (1,\lambda)-ES avec un step-size constant et un (1,\lambda)-ES avec cumulative step-size adaptation sont étudiés dans le cadre de l'optimisation d'une fonction linéaire avec une contrainte linéaire. Avec un step-size constant, l'algorithme résout le problème en divergeant lentement. Sous quelques conditions simples, ce résultat tient aussi lorsque l'algorithme utilise des distributions non Gaussiennes pour générer de nouvelles solutions. En adaptant le step-size avec cumulative step-size adaptation, le succès de l'algorithme dépend de l'angle entre les gradients de la contrainte et de la fonction optimisée. Si celui ci est trop faible, l'algorithme convergence prématurément. Autrement, celui ci diverge log-linéairement.Enfin, les résultats sont résumés, discutés, et des perspectives sur des travaux futurs sont présentées. / In this dissertation an analysis of Evolution Strategies (ESs) using the theory of Markov chains is conducted. Proofs of divergence or convergence of these algorithms are obtained, and tools to achieve such proofs are developed.ESs are so called "black-box" stochastic optimization algorithms, i.e. information on the function to be optimized are limited to the values it associates to points. In particular, gradients are unavailable. Proofs of convergence or divergence of these algorithms can be obtained through the analysis of Markov chains underlying these algorithms. The proofs of log-linear convergence and of divergence obtained in this thesis in the context of a linear function with or without constraint are essential components for the proofs of convergence of ESs on wide classes of functions.This dissertation first gives an introduction to Markov chain theory, then a state of the art on ESs and on black-box continuous optimization, and present already established links between ESs and Markov chains.The contributions of this thesis are then presented:o General mathematical tools that can be applied to a wider range of problems are developed. These tools allow to easily prove specific Markov chain properties (irreducibility, aperiodicity and the fact that compact sets are small sets for the Markov chain) on the Markov chains studied. Obtaining these properties without these tools is a ad hoc, tedious and technical process, that can be of very high difficulty.o Then different ESs are analyzed on different problems. We study a (1,\lambda)-ES using cumulative step-size adaptation on a linear function and prove the log-linear divergence of the step-size; we also study the variation of the logarithm of the step-size, from which we establish a necessary condition for the stability of the algorithm with respect to the dimension of the search space. Then we study an ES with constant step-size and with cumulative step-size adaptation on a linear function with a linear constraint, using resampling to handle unfeasible solutions. We prove that with constant step-size the algorithm diverges, while with cumulative step-size adaptation, depending on parameters of the problem and of the ES, the algorithm converges or diverges log-linearly. We then investigate the dependence of the convergence or divergence rate of the algorithm with parameters of the problem and of the ES. Finally we study an ES with a sampling distribution that can be non-Gaussian and with constant step-size on a linear function with a linear constraint. We give sufficient conditions on the sampling distribution for the algorithm to diverge. We also show that different covariance matrices for the sampling distribution correspond to a change of norm of the search space, and that this implies that adapting the covariance matrix of the sampling distribution may allow an ES with cumulative step-size adaptation to successfully diverge on a linear function with any linear constraint.Finally, these results are summed-up, discussed, and perspectives for future work are explored.

Actuellement, le développement d’un logiciel de taille industriel repose généralement surdes tests ou des preuves unitaires pour garantir rigoureusement ses exigences. En outre, il adéjà été montré que l’utilisation combinée du test et de la preuve unitaires est plus efficaceque l’utilisation d’une seule de ces deux techniques. Néanmoins, un ingénieur en vérificationhésite encore à utiliser ces deux techniques conjointement, faute d’une notion de couverturecommune au test et à la preuve. Définir une telle notion est l’objet de cette thèse.En effet, nous introduisons une nouvelle couverture, appelée « couverture label-mutant ».Elle permet de représenter les critères de couverture structurelle habituels du test, comme lacouverture des instructions, la couverture des branches ou la couverture MC/DC et de décidersi le critère choisi est satisfait en utilisant une technique de vérification formelle, qu’elle soitpar test, par preuve ou par une combinaison des deux. Elle permet également de représenterles critères de couverture fonctionnelle. Nous introduisons aussi dans cette thèse une méthodereposant sur des outils automatiques de test et de preuve pour réduire l’effort de vérificationtout en satisfaisant le critère de couverture choisi. Cette méthode est mise en oeuvre au seinde la plateforme d’analyse de code C (Frama-C), fournissant ainsi à un ingénieur un moyenopérationnel pour contrôler et réaliser la vérification qu’il souhaite. / Currently, industrial-strength software development usually relies on unit testing or unitproof in order to ensure high-level requirements. Combining these techniques has already beendemonstrated more effective than using one of them alone. The verification engineer is yetnot been to combine these techniques because of the lack of a common notion of coverage fortesting and proving. Defining such a notion is the main objective of this thesis.We introduce here a new notion of coverage, named « label-mutant coverage ». It subsumesmost existing structural coverage criteria for unit testing, including statement coverage,branch coverage or MC/DC coverage, while allowing to decide whether the chosen criterionis satisfied by relying on a formal verification technique, either testing or proving or both.It also subsumes functional coverage criteria. Furthermore, we also introduce a method thatmakes use of automatic tools for testing or proving in order to reduce the verification costwhile satisfying the chosen coverage criterion. This method is implemented inside Frama-C, aframework for verification of C code (Frama-C). This way, it offers to the engineer a way tocontrol and to perform the expected verifications.

Nous avons commencé la thèse par la littérature d'enquête sur les approches SPLE et CbyC dans l'état de l'art. Sur la base de l'aperçu et des connaissances obtenues, nous avons analysé les problèmes existants et suggéré des moyens de les résoudre pour notre objectif principal. Nous avons proposé dans le chapitre 2 une méthodologie pour développer des lignes de produits afin que les produits générés soient corrects par construction. Notre intention principale est qu'un utilisateur n'a pas besoin de connaître le processus de génération de produit mais peut recevoir un produit final correct en sélectionnant une configuration de fonctionnalité. En utilisant la méthodologie, les produits finaux sont générés automatiquement et leur exactitude est garantie. À la suite de cette proposition, nous sommes passés au chapitre 3 pour définir la langue de FFML qui est utilisé pour l'écriture de modules. Le mécanisme de réutilisation et de modification, défini pour la langue et appliqué à toutes sortes d'artefacts (spécification, code et preuve de précision) réduit l'effort de programmation. Au chapitre 4, nous nous sommes concentrés sur la définition des mécanismes de composition pour la composition des modules FFML et les intégrons à l'outil FFML Product Generator. L'évaluation de notre méthodologie est réalisée par le développement de deux lignes de produits logiciels, le compte bancaire SPL et le SPL de poker, ce dernier étant un peu plus complexe que le premier. Dans l'évaluation, nous avons souligné les avantages et la limitation de notre méthodologie. / We began the thesis by survey literature on SPLE and CbyC approaches in the State of the Art. Based on the overview and the insights obtained, we have analyzed the existing problems and suggested ways to solve them for our main goal. We have proposed in Chapter 2 a methodology to develop product lines such that the generated products are correct-by-construction. Our main intention is that a user does not need to know the product generation process but can receive a correct final product from selecting a configuration of features. Using the methodology, the final products are generated automatically and their correctness is guaranteed. Following this proposal, we have moved in Chapter 3 to define the FFML language that is used for writing modules. The reuse and modification mechanism, defined for the language and applied to all kinds of artifacts (specification, code and correctness proof), reduce the programming effort. In Chapter 4, we have focused on defining the composition mechanisms for composing FFML modules and embedded them into the FFML Product Generator tool. The evaluation of our methodology is performed through the development of two software product lines, the Bank Account SPL and the Poker SPL, the latter being a bit more complex than the former. In the evaluation, we have highlighted the advantages and the limitation of our methodology.

Cette thèse propose de nouveaux protocoles cryptographiques, plus efficaces que l’existant, et qui permettent aux utilisateurs du nuage informatique (le cloud) de vérifier (i) la bonne conservation des données externalisées et (ii) l'exécution correcte de calculs externalisés. Nous décrivons d'abord un protocole cryptographique qui génère des preuves de récupérabilité, qui permettent aux propriétaires de données de vérifier que le cloud stocke leurs données correctement. Nous détaillons ensuite trois schémas cryptographiques pour vérifier l’exactitude des calculs externalisés en se focalisant sur trois opérations fréquentes dans les procédures de traitement de données, à savoir l’évaluation de polynômes, la multiplication de matrices et la recherche de conjonction de mots-clés. La sécurité de nos solutions est analysée dans le cadre de la sécurité prouvable et nous démontrons également leur efficacité grâce à des prototypes. Nous présentons également A-PPL, un langage de politiques pour l’imputabilité qui permet l'expression des obligations de responsabilité et de traçabilité dans un format compréhensible par la machine. Nous espérons que nos contributions pourront encourager l'adoption du cloud par les entreprises encore réticentes à l’idée d'utiliser ce paradigme prometteur. / This thesis proposes more efficient cryptographic protocols that enable cloud users to verify (i) the correct storage of outsourced data and (ii) the correct execution of outsourced computation. We first describe a cryptographic protocol that generates proofs of retrievability, which enable data owners to verify that the cloud correctly stores their data. We then detail three cryptographic schemes for verifiable computation by focusing on three operations frequent in data processing routines, namely polynomial evaluation, matrix multiplication and conjunctive keyword search. The security of our solutions is analyzed in the provable security framework and we also demonstrate their efficiency thanks to prototypes. We also introduce A-PPL, an accountability policy language that allows the expression of accountability obligations into machine-readable format. We expect our contributions to foster cloud adoption by organizations still wary of using this promising paradigm.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal. / Depuis 1976, les personnes ayant commis un meurtre et condamnées à l'emprisonnement à vie sans possibilité de libération conditionnelle pour une période d'au moins quinze ans peuvent faire réviser ce délai par un juge et jury après avoir purgé quinze ans de cette peine. Le présent mémoire se donne comme objectif général de mieux comprendre ce mécanisme, appelé la révision judiciaire, à travers l'expérience, le point de vue, le vécu et les représentations des avocats ayant piloté de tels dossiers. Pour ce faire, nous avons réalisé des entrevues semi-directives avec des avocats ayant représenté des requérants et la Couronne dans des dossiers québécois. Nous avons également interrogé des avocats des deux parties à l'aide d'entrevues descriptives pour les provinces de l'Alberta, de la Colombie-Britannique, de l'Ontario et de la Saskatchewan. Au total, treize avocats impliqués dans quarante-huit des quatre-vingt-douze dossiers de révision judiciaire ont ainsi été interrogés. Nous avons également analysé le droit s'appliquant à ces dossiers. Cette étude nous a d'abord appris comment les avocats des deux parties se préparaient pour ces dossiers. Ensuite, elle nous donne des informations quant à la manière dont se fait leur preuve, ce qui comprend les différents critères qu'ils voulaient prouver et l'importance qu'ils y accordent, les documents présentés en preuve, les témoins entendus. Troisièmement, nous avons appris quelle était l'attitude des avocats des deux parties à l'égard de cette mesure. Dans un quatrième temps, nous avons obtenu des informations sur la manière dont ils choisissaient un jury. Finalement, nous avons fait ressortir les éléments qui, selon eux, pouvaient avoir une influence sur la décision que le jury rendait. Nous retenons de cette étude que la pratique des avocats de la Couronne du Québec est différente comparativement à leurs confrères des autres provinces canadiennes. Ceci s'expliquant en majeure partie en raison d'une différence d'attitude concernant les fonctions de la peine. Les avocats de la Couronne du Québec interrogés accordent davantage d'importance à la fonction de réhabilitation par opposition à l'effet punitif de la peine, privilégié par leurs confrères des autres provinces. Cette attitude a des répercussions à tous les stades de cette procédure. D'abord, ces derniers consultent tout le dossier carcéral de l'individu. Ensuite, ils entrent en contact avec la famille de la victime. Troisièmement, ils font entendre des témoins plus souvent qu'au Québec. Quatrièmement, ils contestent la majorité des requêtes. Finalement, ils semblent accorder une plus grande importance au critère concernant la nature de l'infraction commise.

La recherche de la vérité est l'objectif du procès pénal dans les modèles accusatoire de common law et inquisitoire. Dans le cadre de notre démonstration, le Canada représente le système accusatoire et la France, un système mixte inspiré du système inquisitoire. Ces modèles mettent donc en place des règles pour éviter une erreur judiciaire. Ces règles exigent que la preuve de la culpabilité emporte la conviction du juge selon un certain degré en fonction du modèle étudié. Pour assurer le respect de ces règles, les procédures canadienne et française utilisent des contrôles indirects et directs du raisonnement du juge des faits. La comparaison permet de déterminer les règles de chaque modèle qui recherchent la vérité et évitent l'erreur judiciaire le plus efficacement.

L’article 6 de la CESDH stipule les principes du procès équitable. Apparemment négligée de ce texte, qui ne la mentionne pas expressément, la matière de la preuve pénale, et des droits qui s’y relient, constitue une composante importante du contentieux issus de l’article 6 Conv. Edh et un domaine dans lequel l’œuvre interprétative de la Cour Edh se fait l’un des laboratoires les plus intéressants pour la comparaison juridique. La « règle de la preuve unique ou déterminante » fixe un standard de garantie minimale, selon lequel la condamnation ne peut pas se fonder, exclusivement ou principalement, sur des éléments de probatoires dont l’administration n’a pas respecté, au niveau interne, les droits que la Convention reconnaît à l’accusé. Élaboré dans un contexte fort innovant, ce critère à la nature juridique hybride, croise, et au même temps sollicite, les tendances évolutives plus récemment à l’œuvre dans le droit probatoire européen. / Article 6 of the ECHR provides the principles of fair trial. Apparently overlooked by this text, which does not explicitly mention it, the field of criminal evidence, and rights in connection therewith, is an important component of litigation from Article 6, and an area in which the European Court of Human Rights interpretative work is one of the most interesting laboratories for legal comparison. The “rule of sole or decisive evidence” establishes a minimum standard of guarantee, by which the conviction cannot be based solely or primarily on evidentiary items whose admission has not respected the conventional rights of the accused. Made in a highly innovative environment, featuring an hybrid legal nature, the “sole or decisive rule” crosses, and at the same time seeks, the more recent evolutionary trends at work in European law of criminal evidence.

Cette thèse s'articule autour de la formalisation de mathématiques dans l'assistant à la preuve Coq dans le but de vérifier des méthodes numériques. Plus précisément, elle se concentre sur la formalisation de concepts qui apparaissent dans la résolution des systèmes d'équations linéaires et non-linéaires. <p> Dans ce cadre, on a analysé la méthode de Newton, couramment utilisée pour approcher les solutions d'une équation ou d'un système d'équations. Le but a été de formaliser le théorème de Kantorovitch qui montre la convergence de la méthode de Newton vers une solution, l'unicité de la solution dans un voisinage, la vitesse de convergence et la stabilité locale de la méthode. L'étude de ce théorème a nécessité la formalisation de concepts d'analyse multivariée. En se basant sur ces résultats classiques sur la méthode de Newton, on a montré qu'arrondir à chaque étape préserve la convergence de la méthode, avec une corrélation bien déterminée entre la précision des données d'entrée et celle du résultat. Dans un travail commun avec Nicolas Julien nous avons aussi formellement étudié les calculs avec la méthode de Newton effectués dans le cadre d'une bibliothèque d'arithmétique réelle exacte. <p> Pour les systèmes linéaires d'équations, on s'est intéressé aux systèmes qui ont une matrice associée à coefficients intervalles. Pour résoudre de tels systèmes, un problème important qui se pose est de savoir si la matrice associée est régulière. On a fourni la vérification formelle d'une collection de critères de régularité pour les matrices d'intervalles.

Le test est l'une des méthodes les plus utilisées pour la validation du logiciel. L'activité de test consiste à exécuter le logiciel sur un sous-ensemble de ses entrées possibles de manière à déceler d'éventuelles erreurs. La présence d'erreurs est établie par confrontation du comportement du logiciel avec un objet de référence. Le processus de test est généralement décomposé en trois phases : la sélection du sous-ensemble des entrées sur lequel le logiciel sera exécuté, la soumission de ces entrées au logiciel en collectant les sorties (les réponses du logiciel) et la décision de l'adéquation de ces sorties avec les sorties attendues.<br /><br />La sélection des données à soumettre au logiciel peut être effectuée selon différentes approches. Lorsque la phase de sélection d'un jeu de tests est opérée à partir d'un objet de référence décrivant plus ou moins formellement le comportement du logiciel, sans connaissance de l'implantation elle-même, on parle de test « boîte noire ». Une des approches de test boîte noire pour laquelle un cadre formel a été proposé est celle qui utilise comme objet de référence une spécification logique du système sous test.<br /><br />Le cadre général de test à partir de spécifications logiques (ou axiomatiques) pose les conditions et les hypothèses sous lesquelles il est possible de tester un système. La première hypothèse consiste à considérer le système sous test comme un modèle formel implantant les opérations dont le comportement est décrit par la spécification. La seconde hypothèse a trait à l'observabilité du système sous test. Il faut fixer la forme des formules qui peuvent être interprétées par le système, c'est-à-dire qui peuvent être des tests. On se restreint généralement au moins aux formules qui ne contiennent pas de variables. Une fois ces hypothèses de test posées, on dispose d'un jeu de tests initial, celui de toutes les formules observables qui sont des conséquences logiques de la spécification. <br /><br />Le premier résultat à établir est l'exhaustivité de cet ensemble, c'est-à-dire sa capacité à prouver la correction du système s'il pouvait être soumis dans son intégralité. Le jeu de tests exhaustif étant le plus souvent infini, une phase de sélection intervient afin de choisir un jeu de tests de taille finie et raisonnable à soumettre au système. Plusieurs approches sont possibles. L'approche suivie dans ma thèse, dite par partition, consiste a diviser le jeu de tests exhaustif initial en sous-jeux de tests, selon un certain critère de sélection relatif à une fonctionnalité ou à une caractéristique du système que l'on veut tester. Une fois cette partition suffisamment fine, il suffit de choisir un cas de test dans chaque sous-jeu de test obtenu en appliquant l'hypothèse d'uniformité (tous les cas de test d'un jeu de test sont équivalents pour faire échouer le système). Le deuxième résultat à établir est que la division du jeu de tests initial n'ajoute pas (correction de la procédure) et ne fait pas perdre (complétude) de cas de test.<br /><br />Dans le cadre des spécifications algébriques, une des méthodes de partition du jeu de tests exhaustif qui a été très étudiée, appelée dépliage des axiomes, consiste à procéder à une analyse par cas de la spécification. Jusqu'à présent, cette méthode s'appuyait sur des spécifications équationnelles dont les axiomes avaient la caractéristique d'être conditionnels positifs (une conjonction d'équations implique une équation).<br /><br />Le travail de ma thèse a eu pour but d'étendre et d'adapter ce cadre de sélection de tests à des systèmes dynamiques spécifiés dans un formalisme axiomatique, la logique modale du premier ordre. La première étape a consisté à généraliser la méthode de sélection définie pour des spécifications équationnelles conditionnelles positives aux spécifications du premier ordre. Ce cadre de test a ensuite été d'adapté à des spécifications modales du premier ordre. Le premier formalisme de spécification considéré est une extension modale de la logique conditionnelle positive pour laquelle le cadre de test a été initialement défini. Une fois le cadre de test adapté aux spécifications modales conditionnelles positives, la généralisation aux spécifications modales du premier ordre a pu être effectuée. <br /><br />Dans chacun de ces formalismes nous avons effectué deux tâches. Nous avons d'une part étudié les conditions nécessaires à imposer à la spécification et au système sous test pour obtenir l'exhaustivité du jeu de tests initial. Nous avons d'autre part adapté et étendu la procédure de sélection par dépliage des axiomes à ces formalismes et montré sa correction et sa complétude. Dans les deux cadres généraux des spécifications du premier ordre et des spécifications modales du premier ordre, nous avons montré que les conditions nécessaires à l'exhausitivité du jeu de test visé étaient mineures car faciles à assurer dans la pratique, ce qui assure une généralisation satisfaisante de la sélection dans ce cadre.