Le travail présenté dans cette thèse est une contribution aux méthodes formelles de spécification et de vérification. Les spécifications formelles sont utilisées pour décrire un logiciel, ou plus généralement un système, d'une manière mathématique sans ambiguïté. Des techniques de vérification formelle sont définies sur la base de ces spécifications afin d'assurer l'exactitude d'un système donné. Cependant, les méthodes formelles ne sont souvent pas pratiques et facile à utiliser dans des systèmes réels. L'une des raisons est que de nombreux formalismes de spécification ne sont pas assez riches pour couvrir à la fois les exigences orientées données et orientées comportement. Certains langages de spécification ont été proposés pour couvrir ce genre d'exigences. Le langage Circus se distingue parmi ces langues par une syntaxe et une sémantique riche et complètement intégrées.L'objectif de cette thèse est de fournir un cadre formel pour la spécification et la vérification de systèmes complexes. Les spécifications sont écrites en Circus et la vérification est effectuée soit par des tests ou par des preuves de théorèmes. Des environnements similaires de spécification et de vérification ont déjà été proposés dans la littérature. Une spécificité de notre approche est de combiner des preuves de théorème avec la génération de test. En outre, la plupart des méthodes de génération de tests sont basés sur une caractérisation syntaxique des langages étudiés. Notre environnement est différent car il est basé sur la sémantique dénotationnelle et opérationnelle de Circus. L'assistant de preuves Isabelle/HOL constitue la plateforme formelle au-dessus de laquelle nous avons construit notre environnement de spécification et de vérification.La première contribution principale de notre travail est l'environnement formel de spécification et de preuve Isabelle/Circus, basé sur la sémantique dénotationnelle de Circus. Sur la base d’Isabelle/HOL nous avons fourni une intégration vérifiée d’UTP, la base de la sémantique de Circus. Cette intégration est utilisée pour formaliser la sémantique dénotationnelle du langage Circus. L'environnement Isabelle/Circus associe à cette sémantique des outils de parsing qui aident à écrire des spécifications Circus. Le support de preuve d’Isabelle/HOL peut être utilisé directement pour raisonner sur ces spécifications grâce à la représentation superficielle de la sémantique (shallow embedding). Nous présentons une application de l'environnement à des preuves de raffinement sur des processus Circus (impliquant à la fois des données et des aspects comportementaux).La deuxième contribution est l'environnement de test CirTA construit au-dessus d’Isabelle/Circus. Cet environnement fournit deux tactiques de génération de tests symboliques qui permettent la vérification de deux notions de raffinement: l'inclusion des traces et la réduction de blocages. L'environnement est basé sur une formalisation symbolique de la sémantique opérationnelle de Circus avec Isabelle/Circus. Plusieurs définitions symboliques et tactiques de génération de test sont définies dans le cadre de CirTA. L'infrastructure formelle permet de représenter explicitement les théories de test ainsi que les hypothèses de sélection de test. Des techniques de preuve et de calculs symboliques sont la base des tactiques de génération de test. L'environnement de génération de test a été utilisé dans une étude de cas pour tester un système existant de contrôle de message. Une spécification du système est écrite en Circus, et est utilisé pour générer des tests pour les deux relations de conformité définies pour Circus. Les tests sont ensuite compilés sous forme de méthodes de test JUnit qui sont ensuite exécutées sur une implémentation Java du système étudié. / The work presented in this thesis is a contribution to formal specification and verification methods. Formal specifications are used to describe a software, or more generally a system, in a mathematical unambiguous way. Formal verification techniques are defined on the basis of these specifications to ensure the correctness of the resulting system. However, formal methods are often not convenient and easy to use in real system developments. One of the reasons is that many specification formalisms are not rich enough to cover both data-oriented and behavioral requirements. Some specification languages were proposed to cover this kind of requirements. The Circus language distinguishes itself among these languages by a rich syntax and a fully integrated semantics.The aim of this thesis is to provide a formal environment for specifying and verifying complex systems. Specifications are written in Circus and verification is performed either by testing or by theorem proving. Similar specifications and verification environment have already been proposed. A specificity of our approach is to combine supports for proofs and test generation. Moreover, most test generation methods are based on a syntactic characterization of the studied languages. Our proposed environment is different since it is based on the denotational and operational semantics of Circus. The Isabelle/HOL theorem prover is the formal platform on top of which we built our specification and verification environment.The first main contribution of our work is the Isabelle/Circus specification and proof environment based on the denotational semantics of Circus. On top of Isabelle/HOL we provide a machine-checked shallow embedding of UTP, the semantics basis of Circus. This embedding is used to formalize the denotational semantics of the Circus language. The Isabelle/Circus environment associates to this semantics some parsing facilities that help writing Circus specifications. The proof support of Isabelle/HOL can be used directly to reason on these specifications thanks to the shallow embedding of the semantics. We present an application of the environment to refinement proofs on Circus processes (involving both data and behavioral aspects). The second main contribution is the CirTA testing framework build on top of Isabelle/Circus. The framework provides two symbolic test generation tactics that allow checking two notions of refinement: traces inclusion and deadlocks reduction. The framework is based on a shallow symbolic formalization of the operational semantics of Circus using Isabelle/Circus. Several symbolic definition and test generation tactics are defined in the CirTA framework. The formal infrastructure allows us to represent explicitly test theories as well as test selection hypothesis. Proof techniques and symbolic computations are the basis of test generation tactics. The test generation environment was used for a case study to test an existing message monitoring system. A specification of the system is written in Circus, and used to generate tests following the defined conformance relations. The tests are then compiled in forms of JUnit test methods and executed against a Java implementation of the monitoring system.This thesis is a step towards, on one hand, the development of sophisticated testing tools making use of proof techniques and, on the other hand, the integration of testing and proving within formally verified software developments.

Cette thèse est composée de deux axes principaux, le premier portant sur le chiffrement homomorphe et le second sur l’algèbre linéaire creuse sur corps finis. Avec l’essor des technologies de communication et en particulier d’internet, de nouveaux protocoles de chiffrement sont développés. En particulier, le besoin de systèmes de chiffrement permettant de manipuler les données chiffrées tout en assurant leur sécurité. C’est dans ce contexte que des systèmes de chiffrement homomorphe sont développés, ces protocoles permettent d’effectuer des calculs avec des données chiffrées. La sécurité de ce type système repose sur l’ajout de bruit aux messages à chiffrer. Ce bruit augmente avec chaque opération effectuée, mais il ne doit pas dépasser un certain seuil. Pour contourner ce problème, une technique nommée bootstrapping est utilisée permettant de réduire le bruit d’un chiffré. Les bootstrappings sont le goulot d’étranglement lors des calculs sur des données chiffrées, il est important d’en faire le moins possible. Or la quantité de bootstrappings à faire est déterminée par la nature des calculs à effectuer ainsi que du protocole de chiffrement utilisé.C’est dans ce contexte que notre travail intervient, nous proposons une méthode effective pour réduire le nombre bootstrappings basé sur la programmation linéaire en nombre entier. Cette méthode s’adapte à un grand nombre de protocoles de chiffrement. De plus, nous effectuons une analyse de la complexité de ce problème en montrant qu’il est APX-complet et nous fournissons un algorithme d’approximation.La résolution de système linéaire sur corps finis est une brique de calcul essentielle dans de nombreux problèmes de calcul formel. En particulier, beaucoup de problèmes produisent des matrices comprenant un grand nombre de zéros, on dit qu’elles sont creuses. Les meilleurs algorithmes permettant de résoudre ce type de système linéaire creux sont des algorithmes dits itératifs. L’opération fondamentale de ces algorithmes itératifs est la multiplication de la matrice par un vecteur ou une matrice dense. Afin d’obtenir les meilleures performances, il est important de tenir compte des propriétés (SIMD, multicoeurs, hiérarchie des caches ....) des processus modernes .C’est dans ce contexte que notre travail intervient, nous étudions la meilleure façon d’implanter efficacement cette opération sur les processeurs récents.Nous proposons un nouveau format permettant de tenir compte du grand nombre de +- 1 présents dans une matrice.Nous proposons une implantation parallèle basée sur le paradigme du vol de tâche offrant un meilleur passage à l’échelle que le parallélisme par threads.Nous montrons comment exploiter au mieux les instructions SIMD des processeurs dans les différentes opérations.Finalement, nous proposons une méthode efficace permettant d’effectuer cette opération lorsque le corps finis est multiprécision (les éléments sont stockés sur plusieurs mots machine) en ayant recours au système de représentation RNS. / This thesis is composed of two independent parts.The first one is related to homomorphic encryption and the second part deal with sparse linear algebra on finite fields.Homomorphic encryption extends traditional encryption in the sense that it becomes feasible to perform operations on ciphertexts, without the knowledge of the secret decryption key. As such, it enables someone to delegate heavy computations on his sensitive data to an untrusted third party, in a secure way. More precisely, with such a system, one user can encrypt his sensitive data such that the third party can evaluate a function on the encrypted data, without learning any information on the underlying plain data. Getting back the encrypted result, the user can use his secret key to decrypt it and obtain, in clear, the result of the evaluation of the function on his sensitive plain data. For a cloud user, the applications are numerous, and reconcile both a rich user experience and a strong privacy protection.The first fully homomorphic encryption (FHE) scheme, able to handle an arbitrary number of additions and multiplications on ciphertexts, has been proposed by Gentry in 2009.In homomorphic encryption schemes, the executed function is typically represented as an arithmetic circuit. In practice, any circuit can be described as a set of successive operation gates, each one being either a sum or a product performed over some ring.In Gentry’s construction, based on lattices, each ciphertext is associated with some noise, which grows at each operation (addition or multiplication) done throughout the evaluation of the function. When this noise reaches a certain limit, decryption is not possible anymore.To overcome this limitation, closely related to the number of operations that the HE.Eval procedure can handle, Gentry proposed in a technique of noise refreshment called“bootstrapping”.The main idea behind this bootstrapping procedure is to homomorphically run the decryptionprocedure of the scheme on the ciphertext, using an encrypted version of the secret key. In this context, our contribution is twofold. We first prove that the lmax-minimizing bootstrapping problem is APX-complete and NP-complete for lmax ≥ 3. We then propose a new method to determine the minimal number of bootstrappings needed for a given FHE scheme and a given circuit.We use linear programming to find the best outcome for our problem. The main advantage of our method over the previous one is that it is highly flexible and can be adapted for numerous types of homomorphic encryption schemes and circuits.Computing a kernel element of a matrix is a fundamental kernel in many computer algebra and cryptography algorithms. Especially, many applications produces matrices with many matrix elements equals to 0.Those matrices are named sparse matrices. Sparse linear algebra is fundamentally relying on iterative approaches such as Wiedemann or Lanczos. The main idea is to replace the direct manipulation of a sparse matrix with its Krylov subspace. In such approach, the cost is therefore dominated by the computation of the Krylov subspace, which is done by successive product of a matrix by a vector or a dense matrix.Modern processor unit characteristics (SIMD, multicores, caches hierarchy, ...) greatly influence algorithm design.In this context our work deal with the best approach to design efficient implementation of sparse matrix vector product for modern processors.We propose a new sparse matrix format dealing with the many +-1 matrix elements to improve performance.We propose a parallel implementation based on the work stealing paradigm that provide a good scaling on multicores architectures.We study the impact of SIMD instructions on sparse matrix operations.Finally, we provide a modular arithmetic implementation based on residue number system to deal with sparse matrix vector product over multiprecision finite fields.

Cette thèse cherche à étudier les liens existants entre les contrats formels et les comportements coopératifs. Les contrats formels étant censés faciliter la collaboration et éviter des incompréhensions coûteuses entre les parties, nous nous intéressons dans un premier temps à la manière dont le contrat formel impacte sur la capacité des parties à coopérer. Nous analysons ensuite, dans un même ordre d’idée, la coopération à travers le prisme des renégociations contractuelles. L’objectif est alors d’étudier la façon dont les contrats s’adaptent à un environnement changeant à travers le temps. Enfin, l’étude se porte sur l’impact de l’existence de rapports informels, considérés par la littérature antérieure comme, de manière alternative, substitut ou complément aux contrats formels. Plus précisément, nous étudions comment l’existence de mécanismes relationnels influe sur les choix contractuels. Ainsi, l’objectif est d’améliorer la compréhension du rôle joué par les contrats formels et la coopération informelle dans les relations et d’enrichir la théorie sur les déterminants de l’incomplétude contractuelle. Nos résultats suggèrent que le rôle du contrat formel dans les relations dépend fortement du contexte et de l’identité des parties concernées. Nos résultats permettent également d’identifier la capacité des parties à soutenir un accord relationnel comme une nouvelle source endogène d’incomplétude contractuelle. Enfin, nous obtenons également que les adaptations contractuelles, par le biais des renégociations, ne sont pas nécessairement nocives pour les parties. Au final, nous pensons que cette thèse contribue à la littérature sur le débat entre complémentarité et / ou substituabilité des modes de gouvernance formels et informels ainsi qu’à la littérature sur le lien entre contrat relationnel et l’incomplétude contractuelle endogène. Par conséquent, l’implication majeure de ce travail de thèse est illustrée par la nécessité pour les parties de réfléchir attentivement au contrat initial et aux efforts consentis pour sa rédaction. En premier lieu car le contrat formel impacte sur leur capacité à coopérer ex post et, en second lieu, car le contrat formel peut se révéler être trop complet par rapport au niveau de complétude optimal. / This Ph.D. dissertation seeks to investigate the existing links between cooperative behavior and formal contracts. First, because formal agreements are supposed to facilitate smooth collaboration and avoid costly misunderstandings, we are interested in how formal contracts impact on the ability of parties to cooperate. Following the same intuition, we also analyze cooperation through the lens of renegotiations in order to investigate how contracts adapt themselves through time in a changing environment. Second, we also study the impact of the existence of informal dealings, alternatively considered in previous literature as substitute or complement to formal contracting. More precisely, we aim to investigate how the existence of relational mechanisms may impact on contractual choices. Our goal is thus to improve the understandings of the role played by formal contract and informal cooperation in relationships and to enrich the theory of the determinants of incomplete contract. Our results suggest that the role of formal contract in relationships strongly depends on the context and the identity of parties. Our results also identify the ability of the parties to sustain a relational agreement as a new source of endogenous contractual incompleteness. Finally, we also find that adaptations through contractual renegotiations are not necessarily harmful for the contracting parties. We believe that this Ph.D. dissertation contributes to the literature on the debate of complementarity and/or the substitutability of formal and informal governance and to the literature on the link between relational contract and endogenous contractual completeness. In the end, the overall implication is the necessity for parties to carefully think about the initial contract they draft. Because it has an impact on their ability to cooperate ex post and also because contracts can be over-complete compared to the efficient (i.e. socially optimal) level of completeness.

: I denna rapport har det gjorts en undersökning om vilket som är det mest lämpliga materialet/ materialen för en handske till formel 1 bilförare. Genom kvalitativa intervjuer och informationsundersökning har en kravspecifikation sammanställts med de viktigaste kraven, som förare och regelverket ställer. Reglerna är angivna i standarder till handskar för formel 1 bilförare. ! En rad olika tester har gjorts och genom det har frågeformuleringarna besvarats. De material som testades var Nomex®, Kevlar®, Trevira CS® och Nomex® III. För att sammanställa alla resultat av testerna har det värderats i två typer av matriser. Den första matrisen som gjordes var en Concept Screening Matrix, där de alternativa materialen fick värden utifrån hur väl de klarade de tre standarder som fanns. På de material som klarade denna matris gjordes sedan en mer detaljerad undersökning, där fanns även förarnas önskemål med som krav på materialen. Dessa tester sammanställdes med olika värden i en Concept Scoring Matrix, resultatet av denna tabell sammanfattar vilket/vilka material som blev svaret på frågeformuleringarna. Det material som efter testerna visade sig vara det mest lämpliga materialet för handskar till formel 1 bilförare var Nomex® och strax efter kom Nomex® III. / Program: Textil produktutveckling och entreprenörskap

Le problème du calcul d'isogénies est apparu dans l'algorithme SEA de comptage de points de courbes elliptiques définies sur des corps finis. L'apparition de nouvelles applications du calcul d'isogénies (crypto système à trappe, fonction de hachage, accélération de la multiplication scalaire, crypto système post quantique) ont motivé par ailleurs la recherche d'algorithmes plus rapides en dehors du contexte SEA. L'algorithme de Couveignes (1996), malgré ses améliorations par De Feo (2011), présente la meilleure complexité en le degré de l'isogénie mais ne peut s'appliquer dans le cas de grande caractéristique.L'objectif de cette thèse est donc de présenter une modification de l'algorithme de Couveignes (1996) utilisable en toute caractéristique avec une complexité en le degré de l'isogénie similaire à celui de Couveignes (1996).L'amélioration de l'algorithme de Couveignes (1996) se fait à travers deux axes: la construction de tours d'extensions de degré $ell$ efficaces pour rendre les opérations plus rapides, à l'image des travaux de De Feo (2011), et la détermination d'ensemble de points d'ordre $ell^k$ stables sous l'action d'isogénies.L'apport majeur de cette thèse est fait sur le second axe pour lequel nous étudions les graphes d'isogénies dans lesquels les points représentent les courbes elliptiques et les arrêtes représentent les isogénies. Nous utilisons pour notre travail les résultats précédents de Kohel (1996), Fouquet et Morain (2001), Miret emph{et al.} (2005,2006,2008), Ionica et Joux (2001). Nous présentons donc dans cette thèse, à l'aide d'une étude de l'action du Frobenius sur les points d'ordre $ell^k$, un nouveau moyen de déterminer les directions dans le graphe (volcan) d'isogénies. / Isogeny computation problem appeared in the SEA algorithm to count the number of points on an elliptic curve defined over a finite field. Algorithms using ideas of Elkies (1998) solved this problem with satisfying results in this context. The appearance of new applications of the isogeny computation problem (trapdoor crypto system, hash function, scalar multiplication acceleration, post quantic crypto system) motivated the search for a faster algorithm outside the SEA context. Couveignes's algorithm (1996) offers the best complexity in the degree of the isogeny but, despite improvements by DeFeo (2011), it proves being unpractical with great characteristic.The aim of this work is to present a modified version of Couveignes's algorithm (1996) that maintains the same complexity in the degree of the isogeny but is practical with any characteristic.Two approaches contribute to the improvement of Couveignes's algorithm (1996) : firstly, the construction of towers of degree $ell$ extensions which are efficient for faster arithmetic operations, as used in the work of De Feo (2011), and secondly, the specification of sets of points of order $ell^k$ that are stable under the action of isogenies.The main contribution of this document is done following the second approach. Our work uses the graph of isogeny where the vertices are elliptic curves and the edges are isogenies. We based our work on the previous results of David Kohel (1996), Fouquet and Morain (2001), Miret emph{& al.} (2005,2006,2008), Ionica and Joux (2001). We therefore present in this document, through the study of the action of the Frobenius endomorphism on points of order $ell^k$, a new way to specify directions in the isogeny graph (volcano).

Les travaux présentés dans ce mémoire portent sur l'étude des langages et méthodes de conception des Systèmes Automatisés de Conception (SAP). Notre objectif est l'amélioration de la rigueur de la définition de ces langages et méthodes. Le moyen retenu est l'utilisation d'un langage formel, le langage Z, pour les méta-modéliser. Dans un premier temps, nous présentons les travaux existants sur l'étude de l'activité de modélisation, afin de montrer l'intérêt de la méta-modélisation vis-à-vis de notre objectif. Dans un deuxième temps, nous caractérisons les différents aspects que doit couvrir un méta-modèle pour représenter avec rigueur un langage ou une méthode. Dans un troisième temps, nous présentons de quelle façon le langage Z permet de couvrir l'ensemble de ces besoins. Nous validons alors notre approche sur deux exemples. Le premier exemple est un langage de conception des systèmes à événements discrets : les réseaux de Petri généralisés. Le deuxième exemple est une méthode de conception de la commande des systèmes hybrides intégrant deux langages : les réseaux de Petri temporels à événements et les équations différentielles.

Le cadre de cette thèse est celui de la théorie des représentations p-adiques, et plus particulièrement la théorie de Fontaine. Je m'intéresse au cas d'une extension métabélienne d'un corps local et construit un (phi, Gamma)-module adapté à cette extension, puis je fournis des généralisations de certains outils usuels associés à ce (phi, Gamma)-module tel qu'un complexe calculant la cohomologie de la représentation. J'établis encore les formules explicites du dictionnaire entre le monde des représentations et celui des (phi, Gamma)-modules, pour le complexe de Herr, le cup-produit ou l'application de Kummer.<br /><br />La seconde partie de ce travail est dévolue à la preuve de la loi de réciprocité de Brückner-Vostokov pour un groupe formel. Je combine pour cela des méthodes relevant des (phi, Gamma)-modules à l'aide des résultats de la première partie et des techniques spécifiques introduites par Abrashkin à travers une interprétation cohomologique de ses travaux. J'obtiens ainsi une preuve de la loi de réciprocité libre de toute hypothèse non naturelle sur l'appartenance de racines de l'unité au corps de base.

Cette thèse est consacrée a l'étude de la forme normale d'Hermite et a la conception d'algorithmes parallèles pour son calcul. Nous avons examine deux cas particuliers: le cas entier et le cas polynomial. Ce problème présente de manière intrinsèque une caractéristique du calcul formel: le grossissement des coefficients intermédiaires. Cette particularité en fait un exemple test pour évaluer la parallélisation en calcul formel. La forme normale d'Hermite pour des matrices a coefficients dans un anneau euclidien est présentée. Les concepts et propriétés sur lesquels sont bases les algorithmes sont décrits. Nous introduisons la théorie sur les réseaux et les problèmes qui lui sont attaches, la forme normale d'Hermite étant une forme canonique du réseau engendre par les colonnes de la matrice initiale. Les différents algorithmes séquentiels sont présentes. Nous étudions et comparons leurs complexités. Puis, une approche parallèle est considérée. Après la présentation des résultats théoriques de nc-réductibilité du problème, nous abordons l'étude de la parallélisation sur modèles expérimentaux. Nous définissons différents algorithmes pour les modèles a mémoire partagée et distribuée. Une implantation a été réalisée sur un hypercube fps t40 (32 processeurs). Le calcul de la forme normale d'Hermite d'une matrice 160160 à coefficients entiers a pu etre effectue en 3 heures. Ce travail s'inscrit dans le cadre du projet massivement Parallele Pac (parallel algebraic computing).

Présentation d'un langage formel pour la spécification des processus communicants. On propose 3 interprétations possibles (modèles) de ce langage: la présentation d'une variété d'algèbres, un système de transition de termes, un arbre (fini ou infini). Introduction d'un calcul pour la construction de réseaux de processus

Réalisation d'un petit système de calcul formel en pascal, sur micro-ordinateur, systeme dénoté SYPAC pour système PASCAL d'aide au calcul formel. Pour décrire les algorithmes de SYPAC on utilise un langage de surface note PALDES pour PASCAL ALDES, dérivant du langage ALDES supportant les systèmes sac-1 et sac-2. On a écrit a partir de la grammaire ll(1) de PALDES un compilateur de ce langage, celui-ci engendre comme code du PASCAL minimal. SYPAC est un systeme modulaire dont la partie résidente est écrite en PASCAL, et les modules recouvrables en PALDES, actuellement deux modules sont implantes : le calcul en précision infinie et le calcul sur les polynômes de z (x). Sa portabilité est assurée par le fait que le PASCAL hôte et l'UCSD PASCAL, disponible sur presque tous les micro-ordinateurs du commerce. L'utilisation prévue de SYPAC est à finalité pédagogique pour l'enseignement secondaire.