Thèse de doctorat : Médecine : Nancy 1 : 2000. / 2000NAN11301. Titre provenant de l'écran-titre.

Il est devenu commun de dire que notre société se transforme inexorablement en une société dite de « l'information ». Cette transformation se caractérise entre autres par une utilisation accrue des technologies de l'information afin de communiquer, d'échanger ou de transiger. Les supports traditionnels de communication (tel que le papier) cèdent progressivement leur place à de nouveaux supports technologiques favorisant l'efficacité et la rapidité des échanges, et par la même occasion le développement du commerce électronique. Qu'on le souhaite ou non, un constat s'impose: la montée en puissance des réseaux virtuels a eu raison du monopole du papier. Sur le plan juridique, cette nouvelle réalité bouleverse aussi considérablement les règles de droit civil largement pensées et ancrées dans un contexte papier. L'avènement de la numérisation et du phénomène de la dématérialisation des supports ont effectivement soulevé plusieurs questions d'ordre juridique tout à fait nouvelles que nous pourrions résumer de la manière suivante: Quels sont les rapports entre l'écrit et son support autre que le papier? Quelles sont les caractéristiques de l'écrit faisant appel aux technologies de l'information? Ce type d'écrit peut-il être admis en tant que moyen de preuve? Si oui, quelle sera sa force probante? Ce type d'écrit doit-il être conservé? Le présent mémoire vise précisément à identifier certains éléments de réponses à ces diverses questions en étudiant spécifiquement les cadres juridiques français et québécois. Ce mémoire traite d'une part des enjeux liés à l'évolution et au rôle de l'écrit face à l'avènement des technologies de l'information et d'autre part du cadre juridique de la preuve et de la conservation de l'écrit dans la société de l'information. / It is becoming commonplace to say that we have entered a so-called "information society". In the process, we have witnessed a transformation characterized by an increased use of information and communication technologies that has revolutionized the way we communicate, learn and conduct business. The traditional communication formats (i.e., paper) gradually yield their place to new technological formats which affect the effectiveness and the speed of transactions, there by enabling the rise of ecommerce. The advent of virtual networks calls into question the monopoly of paper. From a legal perspective, the new paradigm has a huge impact on civil law rules, which were largely anchored in a paper context. The advent of the digitization and the phenomenon of the dematerialization of formats raised several new legal issues that we could summarize in the following manner: What is the relationship between writing and its various formats (e.g., other than paper)? What characterizes writing in an electronic environment? Can this type of writing act as evidence? If so, what will be its conclusive force? How can the integrity of documents be ensured? This thesis examines these various questions within the context of two different legislations: France and Québec. Two issues are addressed: 1) the evolution ofwriting in an electronic, networked environment; 2) the legal framework around evidence and archiving ofwriting in the information society. / "Mémoire présenté à la faculté des études supérieures en vue de l'obtention du grade de maîtrise en droit (L.L.M.)"

L'expertise psychiatrique est requise au tribunal dans plusieurs situations juridiques tant en matière criminelle que civile et elle est soumise aux mêmes règles de preuve que n'importe quelle expertise. Pourtant, la psychiatrie et son objet sont tout à fait particuliers. La relation que peuvent entretenir le juge et l'expert-psychiatre est teintée par plusieurs éléments de nature sociale et professionnelle, mais aussi simplement juridique et procédural. Alors que les juristes parlent de cette relation comme d'une usurpation du rôle du juge par l'expert-psychiatre, les psychiatres, au contraire, croient que leur expertise est totalement pervertie dans le processus judiciaire. Mais la réalité n'est pourtant pas univoque: si l'expertise psychiatrique est de façon générale une preuve parmi les autres, elle peut également occuper une place centrale dans le mécanisme décisionnel. / Psychiatric report is required at the court in several legal statements as weIl in criminal matters as in civic matters and is subject to the same codes of proofs as any other expert report. Still, psychiatry and its object are absolutely peculiar. The relation that may be kept between the judge and the expert psychiatrist is tinged with many elements of social and professional nature but also of judicial and quibbling nature, simply. While lawyers and legal experts quote that relationship of an usurpation of the judge part by the expert psychiatrist , psychiatrists on the other hand reckon that the expert report is completely perverted by the judicial process. Yet, reality is not univocal. If the psychiatric report is globally a proof among many others, it can still have a crucial impact in the ruling machinery. / "Mémoire présenté à la Faculté des études supérieures en vue de l'obtention du grade de maître en droit (LL. M.)". Ce mémoire a été accepté à l'unanimité et classé parmi les 10% des mémoires de la discipline. Commentaires du jury : "Excellent mémoire. Bien construit, bien écrit. Encourageons la candidate à poursuivre au doctorat".

Cette thèse décrit trois travaux de formalisation en Coq. Le premier chapitre s'intéresse à l'implémentation d'une procédure de décision efficace pour les algèbres de Kleene, pour lesquelles le modèle des langages réguliers est initial : il est possible de décider la théorie équationelle des algèbres de Kleene via la construction et la comparaison d'automates finis. Le second chapitre est consacré à la définition de tactiques pour la réécriture modulo associativité et commutativité en utilisant deux composants : une procédure de décision réflexive pour l'égalité modulo AC, ainsi qu'un greffon OCaml implémentant le filtrage modulo AC. Le dernier chapitre esquisse une formalisation des circuits digitaux via un plongement profond utilisant les types dépendants de Coq ; on s'intéresse ensuite à prouver la correction totale de circuits paramétriques.

Cette thèse expose nos travaux de certification d'une partie d'un programme C/C++ nommé SimSoC (Simulation of System on Chip), qui simule le comportement d'archi- tectures basées sur des processeurs tels que ARM, PowerPC, MIPS ou SH4. Un simulateur de System on Chip peut être utilisé pour developper le logiciel d'un système embarqué spécifique, afin de raccourcir les phases des développement et de test, en particulier quand la vitesse de simulation est réaliste (environ 100 millions d'instructions par seconde par cœur dans le cas de SimSoC). Les réductions de temps et de coût de développement obtenues se traduisent par des cycles de conception interactifs et rapides, en évitant la lourdeur d'un système de développement matériel. SimSoC est un logiciel complexe, comprenant environ 60 000 de C++, intégrant des parties écrites en SystemC et des optimisations non triviales pour atteindre une grande vitesse de simulation. La partie de SimSoC dédiée au processeur ARM, l'un des plus répandus dans le domaine des SoC, transcrit les informations contenues dans un manuel épais de plus de 1000 pages. Les erreurs sont inévitables à ce niveau de complexité, et certaines sont passées au travers des tests intensifs effectués sur la version précédente de SimSoC pour l'ARMv5, qui réussissait tout de même à simuler l'amorçage complet de linux. Un problème critique se pose alors : le simulateur simule-t-il effectivement le matériel réel ? Pour apporter des éléments de réponse positifs à cette question, notre travail vise à prouver la correction d'une partie significative de SimSoC, de sorte à augmenter la confiance de l'utilisateur en ce similateur notamment pour des systèmes critiques. Nous avons concentré nos efforts sur un composant particulièrement sensible de SimSoC : le simulateur du jeu d'instructions de l'ARMv6, faisant partie de la version actuelle de SimSoC. Les approches basées sur une sémantique axiomatique (logique de Hoare par exemple) sont les plus répandues en preuve de programmes impératifs. Cependant, nous avons préféré essayer une approche moins classique mais plus directe, basée sur la sémantique opérationnelle de C : cela était rendu possible en théorie depuis la formalisation en Coq d'une telle sémantique au sein du projet CompCert et mettait à notre disposition toute la puissance de Coq pour gérer la complexitité de la spécification. À notre connaissance, au delà de la certification d'un simulateur, il s'agit de la première expérience de preuve de correction de programmes C à cette échelle basée sur la sémantique opérationnelle. Nous définissons une représentation du jeu d'instruction ARM et de ses modes d'adressage formalisée en Coq, grâce à un générateur automatique prenant en entrée le pseudo-code des instructions issu du manuel de référence ARM. Nous générons égale- ment l'arbre syntaxique abstrait CompCert du code C simulant les mêmes instructions au sein de Simlight, une version allégée de SimSoC. À partir de ces deux représentations Coq, nous pouvons énoncer et démontrer la correction de Simlight, en nous appuyant sur la sémantique opérationnelle définie dans CompCert. Cette méthodologie a été appliquée à au moins une instruction de chaque catégorie du jeu d'instruction de l'ARM. Au passage, nous avons amélioré la technologie disponible en Coq pour effectuer des inversions, une forme de raisonnement utilisée intensivement dans ce type de situation.

Thèses (LL.M.)--Université de Sherbrooke (Canada), 1997. / Titre de l'écran-titre (visionné le 20 juin 2006). Publié aussi en version papier.

Lorsqu'une infraction est comme, la recherche de son auteur est non seulement une question factuelle mais aussi une question juridique centrale dans la procédure pénale. dans une société démocratique, l'appréhension de l'auteur de l'infraction exige la preuve de sa participation aux faits.la police judiciaire a pour mission de constater les infractions pénales et de procéder aux investigations nécessaires à la manifestation de la vérité. en d'autres termes, elle doit rapporter la preuve de la commission de l'infraction et de son imputation à une ou plusieurs personnes déterminées. / Criminal proceedings must meet two requirements:- Ensure investigating authorities broad and powerful means of investigation.- Protect individuals from the danger of arbitrariness with their freedom and unfounded conviction.Those two requirements are faced with great acuity in special proceedings right. Now the principle of proportionality between the seriousness of the offense and the procedure is applied.The offenses related to a crime considered as serious (as organized criminality) are subjected to a special procedure facilitating the taking of evidence and decreasing the individual freedom protection.The following research attempts to identify explicit and implicit criteria of this principle of proportionality in criminal proceedings throughout the regime of the taking of evidence by judicial police.

En informatique comme dans de multiples autres domaines, les graphes peuvent être trouvés partout. Ils sont utilisés pour représenter des données dans des domaines allant de la chimie à l'architecture, en tant que structures abstraites ou que modèles des données et de leurs évolutions. Dans tous ces domaines, il est prévisible que les graphes évoluent au cours du temps suite à des réactions chimiques, une mise à jour des connaissance ou l'exécution d'un programme. Être capable de traiter ces transformations est une tâche particulièrement importante et difficile. Dans ce travail, notre objectif est d'étudier la vérification de telles transformations de graphes, c'est à dire comment prouver qu'une transformation de graphes est correcte. La correction d'une transformation est plus précisément définie comme la correction d'une spécification pour cette transformation contenant en plus une précondition et une postcondition. Nous avons décidé d'utiliser un calcul à la Hoare générant une plus faible précondition pour une postcondition et une transformation. Si cette plus faible précondition est impliquée par la précondition, la spécification est correcte. Nous avons choisi une approche plus algorithmique pour les transformation de graphes utilisant des actions atomiques. Nous définissons deux moyens de construire des transformations de graphes: en utilisant un langage impératif ou en utilisant des systèmes de règles de réécriture. Le principal ingrédient est la logique qui est choisie pour représenter la précondition, la postcondition et les possibles conditions internes. Pour que la logique puisse interagir avec le calcul, nous demandons que le problème de décision soit décidable, qu'elle soit fermée par substitutions et qu'elle soit capable d'exprimer l'existence ou l'absence d'un sous-graphe affecté par la transformation. Le résultat central de ce travail est l'identification et l'explication de ces conditions. / In computer science as well as multiple other fields, graphs have become ubiquitous. They are used to represent data in domains ranging from chemistry to architecture, as abstract structures or as models of the data or its evolution. In all these domains, graphs are expected to evolve over time due to chemical reactions, update of the knowledge or programs. Being able to deal with such transformations is an extremely important and difficult task. In this work, our aim is to study the verification of such graph transformation, that is how to prove that a graph transformation is correct. Correctness of a graph transformation is more precisely defines as correctness of a specification for the transformation containing additionally a precondition and a postcondition. We decided to use a Hoare-like calculus generating the weakest precondition for a postcondition and a transformation. If this weakest precondition is implied by the actual precondition, the specification is correct. We chose a more algorithmic approach to graph transformation by using atomic actions.We chose to define two ways to build graph transformations: using an imperative programming language and using rule-base rewriting systems. The main ingredient of the verification of graph transformation is the logic that is chosen to represent the precondition, the postcondition and the possible conditions internal to the transformation. So that the logic can interact with the calculus, we require that the decision problem be decidable, that the logic be closed under the substitutions introduced by the Hoare-like calculus and that it has to be able to express the existence and absence of a match for the transformation. The core result of this work is the identification and explanation of these conditions.

Concevoir et implanter des programmes parallèles est une tâche complexe, sujette aux erreurs. La vérification des programmes parallèles est également plus difficile que celle des programmes séquentiels. Pour permettre le développement et la preuve de correction de programmes parallèles, nous proposons de combiner le langage parallèle fonctionnel quasi-synchrone BSML, les squelettes algorithmiques - qui sont des fonctions d’ordre supérieur sur des structures de données réparties offrant une abstraction du parallélisme – et l’assistant de preuve Coq, dont le langage de spécification est suffisamment riche pour écrire des programmes fonctionnels purs et leurs propriétés. Nous proposons un plongement des primitives BSML dans la logique de Coq sous une forme modulaire adaptée à l’extraction de programmes. Ainsi, nous pouvons écrire dans Coq des programmes BSML, raisonner dessus, puis les extraire et les exécuter en parallèle. Pour faciliter le raisonnement sur ceux-ci, nous formalisons le lien entre programmes parallèles, manipulant des structures de données distribuées, et les spécifications, manipulant des structures séquentielles. Nous prouvons ainsi la correction d’une implantation du squelette algorithmique BH, un squelette adapté au traitement de listes réparties dans le modèle de parallélisme quasi synchrone. Pour un ensemble d’applications partant d’une spécification d’un problème sous forme d’un programme séquentiel simple, nous dérivons une instance de nos squelettes, puis nous extrayons un programme BSML avant de l’exécuter sur des machines parallèles. / Parallel program design and implementation is a complex, error prone task. Verifying parallel programs is also harder than verifying sequential ones. To ease the development and the proof of correction of parallel programs, we propose to combine the functional bulk synchronous parallel language BSML; the algorithmic skeleton, that are higher order function on distributed data structures which offer an abstraction of the parallelism ; and the Coq proof assistant, who’s specification language is rich enough to write purely functional programs together with their properties. We propose an embedding of BSML primitives in the Coq logic in a modular form, adapted to program extraction. So we can write BSML programs in Coq, reason on them, extract them and then execute them in parallel. To ease the specification of these programs, we formalise the relation between parallel programs using distributed data structures and specification using sequential data structure. We prove the correctness of an implementation of the BH skeleton. This skeleton is devoted to the treatment of distributed lists in the BSP model. For a set of application, starting from a sequential specification of a problem, we derive an instance of our skeletons, then extract a BSML program which is executed on parallel machines.

Les applications informatiques sont de plus en plus présentes dans nos vies. Pour les applications critiques (médecine, transport, . . .), les conséquences d’une erreur informatique ont un coût inacceptable, que ce soit sur le plan humain ou financier. Une des méthodes pour éviter la présence d’erreurs dans les programmes est la vérification déductive. Celle-ci s’applique à des programmes écrits dans des langages de haut-niveau transformés, par des compilateurs, en programmes écrits en langage machine. Les compilateurs doivent être corrects pour ne pas propager d’erreurs au langage machine. Depuis 2005, les processeurs multi-coeurs se sont répandus dans l’ensemble des systèmes informatiques. Ces architectures nécessitent des compilateurs et des preuves de correction adaptées. Notre contribution est l’extension modulaire d’un compilateur vérifié pour un langage parallèle ciblant des architectures parallèles multi-coeurs. Les spécifications des langages (et leurs sémantiques opérationnelles) présents aux divers niveaux du compilateur ainsi que les preuves de la correction du compilateur sont paramétrées par des modules spécifiant des éléments de parallélisme tels qu’un modèle mémoire faible et des notions de synchronisation et d’ordonnancement entre processus légers. Ce travail ouvre la voie à la conception d’un compilateur certifié pour des langages parallèles de haut-niveau tels que les langages à squelettes algorithmiques. / Nowadays, we are using an increasing number of computer applications. Errors in critical applications (medicine, transport, . . .) may carry serious health or financial issues. Avoiding errors in programs is a challenge and may be achieved by deductive verification. Deductive verification applies to program written in a high-level languages, which are transformed into machine language by compilers. These compilers must be correct to ensure the nonpropagation of errors to machine code. Since 2005, multicore processors have spread in all electronic devices. So, these architectures need adapted compilers and proofs of correctness. Our work is the modular extension of a verified compiler for parallel languages targeting multicore architectures. Specifications of these languages (and their operational semantics) needed at all levels of the compiler and proofs of correctness of this compiler are parameterized by modules specifying elements of parallelism such as a relaxed memory model and notions of synchronization and scheduling between threads. This work is the first step in the conception of a certified compiler for high-level parallel languages such as algorithmic skeletons.