This thesis is based on a study of reproducibility issues in image processing research. We designed, created and developed a scientific journal, Image Processing On Line (IPOL), in which articles are published with a complete implementation of the algorithms described, validated by the rapporteurs. A demonstration web service is attached, allowing testing of the algorithms with freely submitted data and an archive of previous experiments. We also propose copyrights and license policy, suitable for manuscripts and research software software, and guidelines for the evaluation of software. The IPOL scientific project seems very beneficial to research in image processing. With the detailed examination of the implementations and extensive testing via the demonstration web service, we publish articles of better quality. IPOL usage shows that this journal is useful beyond the community of its authors, who are generally satisfied with their experience and appreciate the benefits in terms of understanding of the algorithms, quality of the software produced, and exposure of their works and opportunities for collaboration. With clear definitions of objects and methods, and validated implementations, complex image processing chains become possible.

With the development of digital networks, such as Internet, communication protocols are omnipresent. Digital devices have to interact with each other in order to perform the numerous and complex tasks we have come to expect as commonplace, such as using a mobile phone, sending or receiving electronic mail, making purchases online and so on. In such applications, security is important. For instance, in the case of an online purchase, the right amount of money has to be paid without leaking the buyer personal information to outside parties. Communication protocols are the rules that govern these interactions. In order to make sure that they guarantee a certainlevel of security, it is desirable to analyze them. Doing so manually or by testing them is not enough, as attacks can be quite subtle. Some protocols have been used for years before an attack was discovered. Because of their increasing ubiquity in many important applications, e.g. electronic commerce, a very important research challenge consists in developing methods and verification tools to increase our trust on security protocols, and so on the applications that rely on them. For example, more than 28 billion Euros were spent in France using Internet transactions, and the number is growing. Moreover, new types of protocols are continuously appearing in order to face new technological and societal challenges, e.g. electronic voting, electronic passport to name a few.

This thesis is about the formal verification and composition of security protocols, motivated by applications to electronic voting protocols. Chapters 3 to 5 concern the verification of security protocols while Chapter 6 concerns composition.We show in Chapter 3 how to reduce certain problems from a quotient term algebra to the free term algebra via the use of strongly complete sets of variants. We show that, when the quotient algebra is given by a convergent optimally reducing rewrite system, finite strongly complete sets of variants exist and are effectively computable.In Chapter 4, we show that static equivalence for (classes of) equational theories including subterm convergent equational theories, trapdoor commitment and blind signatures is decidable in polynomial time. We also provide an efficient implementation.In Chapter 5 we extend the previous decision procedure to handle trace equivalence. We use finite strongly complete sets of variants introduced in Chapter 3 to get rid of the equational theory and we model each protocol trace as a Horn theory which we solve using a refinement of resolution. Although we have not been able to prove that this procedure always terminates, we have implemented it and used it to provide the first automated proof of vote privacy of the FOO electronic voting protocol.In Chapter 6, we study composition of protocols. We show that two protocols that use arbitrary disjoint cryptographic primitives compose securely if they do not reveal or reuse any shared secret. We also show that a form of tagging is sufficient to provide disjointness in the case of a fixed set of cryptographic primitives.

In this thesis we investigate the expressive power of several logics over finite trees. In particular we want to understand precisely the expressive power of first-order logic over finite trees. Because we study many logics, we proceed by comparison to a logic that subsumes them all and serves as a yardstick: monadic second-order logic. Each logic we consider is a fragment of monadic second-order logic. MSO is linked to the theory of formal languages. To each logical formula corresponds a tree language, which is the language of trees satisfying this formula. Furthermore, given a logic we can associate a class of tree languages: the class of languages definable by a formula of this logic. In the setting of finite trees MSO corresponds exactly to the class of regular tree languages. Given a logic, we actually look for a decidable characterization of the class of languages defined in this logic. By decidable characterization, we mean an algorithm for solving the following problem: given as input a finite tree automaton, decide if the recognized language belongs to the class in question. We will actually obtain our decidable characterizations by exhibiting for each class a set of closure properties such that a language is in the class under investigation if and only if it satisfies these closure properties. Each such closure property is then shown to be decidable. Stating and proving such closure properties usually yields a solid understanding of the expressive power of the corresponding logic. The main open problem in this research area is to obtain a decidable characterization for the class of tree languages that are definable in first-order logic. We provide decidable characterizations for several fragments of FO. First we provide three decidable characterizations for classes of regular languages of trees of bounded rank. The first class we consider is the class of languages definable in the temporal logic EF+F^-1. It essentially navigates the trees using two modalities for moving to a descendant node or an ancestor node. The second class we consider is the class of trees of bounded rank definable using one quantifier alternation. The last class, is the class of languages definable using a boolean combination of existential first order formulas. In the setting of forests, we investigate the class of languages definable in first-order logic using only two variables and two prediactes corresponding respectively to the ancestor and following sibling relations. We provide a characterization for this logic. The last class for which we provide a decidable characterization is the class of locally testable language (LT). A language L is in LT if membership in L depends only on the presence or absence of neighborhoods of a certain fixed size in the tree. We define notions of LT for both unranked trees and trees of bounded rank by adapting the definition of neighborhood to each setting. Then we provide a decidable characterization for both notions of LT.

Nous etendons les logiques temporelles du temps alternant ATL et ATL* au moyen de contextes strategiques et de contraintes sur la memoire : la premiere extension permet aux agents de s'en tenir a leurs strategies lors de l'evaluation des formules, contrairement a ATL ou chaque quantificateur de strategies ecrase les strategies anterieurement selectionnees. La seconde extension permet aux quantificateurs de strategies de se restreindre aux strategies sans memoire ou avec memoire bornee. Nous avons l'etudie l'expressivite de nos logiques. Nous montrons qu'elles expriment des proprietes importantes comme l'exstence d'equilibres, et nous les comparons formellement a d'autres formalismes proches (ATL, ATL*, Game Logic, Strategy Logic, ...). Nous avons aborde les problemes de model-checking. Nous donnons un algorithme PSPACE pour la logique n'impliquant que des strategies sans memoire, et un algorithme EXPSPACE pour le cas des strategies a memoire bornee. Dans le cas general, malgre leur forte expresssivite, nous prouvons que leur model-checking reste decidable par un algorithme a base d'automates d'arbres alternants qui permet d'evaluer une formule sur la classe complete des CGS avec n joueurs.

Les langages synchrones ont été fondés pour modéliser et implémenter les systèmes réactifs temps-réels critiques. Avec la complexité toujours croissante des systèmes contrôlés, la vitesse d'exécution devient un critère important. Nous sommes donc à la recherche d'une exécution parallèle, combinant efficacité et sûreté.Les langages synchrones ont toujours intégré la notion de parallélisme, mais ce, pour l'expressivité de la modélisation. Leurs compilations visent principalement les circuits ou la génération de code séquentiel. Tous ont une sémantique formelle, qui rend possible la distribution correcte du code. Mais la préservation de cette sémantique peut être un obstacle à l'efficacité du code généré, particulièrement s'il est nécessaire de préserver une notion d'instant global au système.Le modèle sémantique qui nous intéresse est celui des réseaux de Kahn. Ces réseaux modélisent des calculateurs distribués, communiquant au travers de files de taille non bornée. Dans ce cadre, la distribution ne demande aucune communication ni synchronisation supplémentaire. En considérant l'histoire des files de communication, la sémantique de Kahn permet de s'abstraire de l'exécution effective, tout en garantissant le déterminisme du calcul. Pour cela, chaque nœud du réseau doit avoir une sémantique fonctionnelle continue.Le langage que nous développons est Heptagon, un langage synchrone fonctionnel du premier ordre, déscendant de Lustre. Son compilateur est un prototype universitaire, apparenté à l'outil industriel Scade. Grâce à sa sémantique de Kahn, la distribution d'un programme Heptagon ne pose pas de question, son efficacité beaucoup plus.L'efficacité requiert de minimiser les synchronisations. Cela revêt deux aspects non indépendants. Avoir un découplage suffisant des calculs : il y a des délais dans les dépendances entre calculs. Avoir une granularité importante des calculs : un fort ratio temps de calcul sur fréquence de communication. Or la sémantique synchrone et les horloges d'un programme Heptagon reflètent exactement l'inverse. Elles permettent au programmeur de se contenter d'un découplage d'un instant et à chaque instant, au maximum une valeur est calculée. De plus, les instants sont typiquement courts, pour assurer que le système réagit rapidement.Des précédents travaux sur le sujet, nous tirons deux constats.Le premier est que nous souhaitons le contrôle du parallélisme par le programmeur, directement dans le code source. Il doit pouvoir maîtriser à quels instants il y a communication ou synchronisation. La solution que nous proposons dans ce manuscrit est l'utilisation des futures dans Heptagon. Ils fournissent ce pouvoir au programmeur, tout en restant des annotations qui peuvent être supprimées sans changer la sémantique dénotationnelle du programme.Le deuxième constat est que la question de la granularité des calculs est une question profonde, touchant en particulier aux questions de dépendance de données, de choix des horloges et de compilation modulaire. Heptagon, comme ses parents, restreint les réseaux de Kahn qui peuvent être écrits, de telle sorte que ces trois questions se traitent séparément. Pour mieux comprendre le lien entre ces éléments, nous revenons aux réseaux de Kahn. Notre principal résultat est la définition de la sous-classe des réseaux ordonnés réactifs. Ceux-ci sont les seuls pour lesquels nous pouvons décrire modulairement le comportement avec des horloges, sans restreindre les contextes d'appels. Ces réseaux ont une signature d'horloge en forme normale, qui maximise la granularité. Pour l'exprimer, nous introduisons les horloges entières, décrivant la communication de plusieurs valeurs en un seul instant. Nous appliquons ensuite nos résultats pour voir sous un nouveau jour Heptagon, Signal, les politiques des objets de Lucid Synchrone, mais aussi proposer une analyse pleinement modulaire de Lucy-n langage synchrone le plus fidèle aux réseaux de Kahn.

Nous développons une approche générique pour comprendre comment différents régimes alimentaires peuvent influencer la qualité et la composition du lait. Cette question s'intègre dans le cadre du Flux Balance Analysis (FBA), qui consiste à analyser un réseau métabolique en optimisant un système de contraintes linéaires. Nous avons proposé une extension du FBA pour analyser la transformation des nutriments en intégrant des hypothèses biologiques utilisées par différents modèles numériques dans un modèle générique de la glande mammaire. Notre méthode permet de quantifier les précurseurs qui interviennent dans la composition des sorties du système, en calculant des contributions des entrées dans les sorties [AIO]. A l'aide de cette approche, nous avons montré que la transformation des nutriments du lait ne peut pas être modélisée par l'optimisation d'une combinaison linéaire des flux des réactions sur un modèle du métabolisme mammaire. Pour étudier plus précisément la flexibilité d'un réseau métabolique, nous avons proposé un algorithme efficace de recherche locale pour calculer les valeurs extrémales des coefficients des AIOs. Cette approche permet de discriminer les traitements sans formuler d'hypothèses sur le comportement interne du système.

Les problèmes d'optimisation discrète sont pour beaucoup difficiles à résoudre, depar leur nature combinatoire. Citons par exemple les problèmes de programmationlinéaire en nombres entiers. Une approche couramment employée pour les résoudreexactement est l'approche de Séparation et Évaluation Progressive. Une approchedifférente appelée " Resolution Search " a été proposée par Chvátal en 1997 pourrésoudre exactement des problèmes d'optimisation à variables 0-1, mais elle restemal connue et n'a été que peu appliquée depuis.Cette thèse tente de remédier à cela, avec un succès partiel. Une première contributionconsiste en la généralisation de Resolution Search à tout problème d'optimisationdiscrète, tout en introduisant de nouveaux concepts et définitions. Ensuite,afin de confirmer l'intérêt de cette approche, nous avons essayé de l'appliquer enpratique pour résoudre efficacement des problèmes bien connus. Bien que notrerecherche n'ait pas abouti sur ce point, elle nous a amené à de nouvelles méthodespour résoudre exactement les problèmes d'affectation généralisée et de localisationsimple. Après avoir présenté ces méthodes, la thèse conclut avec un bilan et desperspectives sur l'application pratique de Resolution Search.

Pouvoir lutter efficacement contre certains fléaux comme les incendies de forêt, les feux de brousse ou les catastrophes naturelles constitue un enjeu majeur dans plusieurs villes du monde.Avec l'avènement de la technologie de pointe représentée par les réseaux de capteurs, la détection de ces phénomènes devient plus aisée.En effet, des capteurs peuvent être déployés dans des zones difficiles d'accès et s'ils sont suffisamment nombreux pour couvrir la totalité de l'environnement à surveiller, une alerte peut être directement donnée par le capteur ayant détecté un certain type d'évènement (feu, secousse sismique...).Le centre de contrôle ayant reçu l'alerte peut ensuite décider d'intervenir sur la zone en cause.Nos travaux se situent dans ce cadre de la détection de phénomènes par un réseau de capteurs, en supposant que l'environnement est connu et que les capteurs sont mobiles, sans fil et en nombre insuffisant pour couvrir la totalité de l'environnement à surveiller.Parler de surveillance par un nombre faible d'entités mobiles nécessite de parcourir régulièrement certaines zones critiques de l'environnement, ce qui peut s'apparenter à une tâche de patrouille.Dans le cadre de cette thèse, nous nous sommes focalisés sur la détermination de stratégies de patrouille multi-capteurs appliquée à la détection d'évènements.Un problème similaire au nôtre est celui de la patrouille multi-agents dans un environnement connu.Ce problème consiste à faire visiter régulièrement les noeuds d'un graphe (représentant l'environnement) par des agents.Les capteurs peuvent être considérés comme des agents ayant des ressources limitées, en terme d'énergie en particulier.Le cadre de la patrouille multi-agents et les techniques proposées pour le résoudre ne peuvent pas être utilisés ici.Après avoir formulé mathématiquement le problème de la patrouille multi-capteurs appliquée à la détection d'évènements, nous proposons une technique de résolution approchée basée sur des colonies de fourmis.Des simulations ont été réalisées en considérant différents scenarii (topologies d'environnement, populations de capteurs, apparitions des événements) afin d'évaluer la pertinence de notre approche.Les résultats expérimentaux montrent que notre approche permet de déterminer des stratégies de patrouille satisfaisantes dans la majorité des scenarii.

L'analyse statique de programmes est un domaine crucial en compilation, en optimisation, et en validation de logiciels. Les structures de données complexes (tableaux, listes, graphes,...), omniprésentes dans les programmes, posent des problèmes difficiles, du fait qu'elles représentent des ensembles de données de taille importante ou inconnue, et que l'adressage des données dans ces ensembles est calculé (indexation, indirection). Si la vérification de la validité des accès aux tableaux a été l'une des motivations initiales de l'interprétation abstraite, la recherche de propriétés concernant le contenu des tableaux est quant à lui un sujet récent. La plupart des travaux sur le sujet reposent sur un partitionnement des tableaux. On est ainsi amenés à considérer un certain nombre de fragments de tableau desquels on cherche à trouver des propriétés. Le choix de cette partition est un problème difficile et chacune des méthodes proposées peut être mise en défaut. Par ailleurs, les représentations classiques des partitions de tableau donnent à ces analyses une complexité exponentielle. Nous proposons d'une part de généraliser le concept de partitionnement de tableau à celui de "fragmentation" permettant à la fois le chevauchement des fragments, la manipulation de fragments potentiellement vides et la sélection de relations spécialisées. D'autre part, nous proposons une abstraction de ces fragmentations en terme de graphes appelés "Diagrammes de tranches" ainsi que les opérations pour les manipuler et assurant une complexité polynomiale à l'analyse. Enfin, nous proposons un nouveau critère de fragmentation sémantique inspiré de ceux de la littérature et tentant d'en corriger les défauts. Ces méthodes ont été implémentées dans un analyseur statique. L'expérimentation démontre qu'elles peuvent analyser avec efficacité et précision un certain nombre d'exemples constituant des défis de l'analyse statique de programmes manipulant des tableaux.