Dans le cadre du développement et de la vérification formelle d'un compilateur pour langage fonctionnel, nous avons fait l'expérience de l'influence de la preuve de préservation sémantique sur la conception des langages intermédiaires et de leurs sémantiques formelles.
Il s'agit d'un compilateur pour le fragment purement fonctionnel de ML, non typé, vérifié formellement dans l'assistant de preuves Coq. Dans l'esprit des compilateurs CompCert, ce compilateur est réaliste et optimisant. En plus d'une grande expressivité du langage source (fonctions récursives, type concret et filtrage) et de l'implantation d'optimisations (décurryfication, CPS, compilation optimisée des appels en position terminale), nous proposons une interaction avec un gestionnaire de mémoire automatique à glanneur de cellules.
Plus concrètement, nous avons développé une chaîne de compilation en amont dont le langage cible est Cminor, le langage d'entrée du backend CompCert, ce qui nous permet de produire du code en assembleur PowerPC. Notre chaîne de compilation en amont est une séquence de plusieurs transformations de langages intermédiaires. Pour chacune de ces transformations, nous avons montré un résultat de préservation sémantique. La composition de ces résultats nous mène à la vérification formelle de notre compilateur.
Dans cet exposé, nous proposons une vue d'ensemble de ce compilateur et détaillons deux points importants. Le premier concerne la décurryfication, qui est celle implantée dans le système Objective Caml. Le second est la vérification formelle de l'interaction avec un gestionnaire de mémoire automatique au travers de deux transformations mettant en jeu uniquement des langages purement fonctionnels.
The idea of an incremental application of different termination techniques as processors for solving termination problems has shown to be a powerful and efficient way to prove termination of rewriting. Nowadays, the dependency pair framework (which develop this idea) is the most succesful approach for proving termination of rewriting. The DP-framework relies on the notion of dependency pair to decompose a termination problem into a set of dependency pair termination problems (DP-termination problems). These problems can be treated independently by appplying different dependency pair processors (DP-processors). If we prove (disprove) the termination of all (some) of the DP-problems, we can ensure that the system is terminating (nonterminating). Context-sensitive rewriting (CSR) is a restriction of rewriting that forbids reductions on some subexpressions and that has been proved useful to model and analyze programming language features at different levels. Advances in dependency pair techniques related with context-sensitive rewriting (CSR) are growing fast in the last years. The definition of a context-sensitive dependency pair (CSDP) framework for CSR becomes necessary to benefit from these new techniques and approaches in the realm of CSR termination techniques. In this thesis, we show how to develop a dependency pair framework for proving termination of CSR.
We present a new approach for proving termination of term rewrite systems that uses polynomial interpretations together with the "maximum" function. To obtain a powerful automatic method, we show how to automate the search for such interpretations by integrating "max" into recent SAT-based methods for polynomial interpretations.
Furthermore, not only can the power of polynomial interpretations be increased by changing the shape of the interpretation (e.g., by using the "maximum" function), but also by using interpretations into a different domain, such as the rationals. We present SAT-based methods for finding such rational polynomial interpretations efficiently.
We implemented our contributions in the termination prover AProVE, and experimental results show that both approaches lead to further increases in termination proving power.
Le logiciel embarqué a pris une place importante dans les automobiles modernes. Puisqu'un véhicule doit présenter une bonne sûreté de fonctionnement, il semblerait normal que des méthodes extrêmement formelles soient utilisées. Or, ce n'est pas le cas, en tous cas pas dans la grande majorité des projets automobiles.
Ce séminaire a pour objectifs :
On présente SAD (System for Automated Deduction), un assistant de preuve destiné à la vérification de textes mathématiques formalisés. Dans SAD, le texte à vérifier est écrit dans ForTheL, un langage formel proche de la langue naturelle et le style des publications mathématiques. En dehors de présenter une interface amicale à l'utilisateur, notre intention est d'exploiter les indices que la forme « humaine » du problème nous donne : les définitions, les schémas de preuve, les substantifs qui désignent des classes d'objets, etc.
La vérification consiste en la démonstration que le texte est « sensé » et « fondé », c'est-à-dire que les fonctions et les relations sont employées dans leurs domaines, conformément aux définitions, et les assertions se déduisent des prémisses. La définition formelle d'un texte correct repose sur un calcul séquentiel cohérent ainsi que sur la notion de validité locale (par rapport à une occurrence à l'intérieur d'une formule). Les propositions locales nous permettent, en particulier, de raisonner sur les objets typés dans un langage sans types.
SAD effectue la recherche de preuve à deux niveaux. Le niveau bas est un démonstrateur automatique combinatoire pour la logique classique du premier ordre, tel que SPASS ou Otter. Le niveau haut est un « raisonneur » qui emploie des techniques naturelles de démonstration pour filtrer, simplifier, décomposer une tâche de preuve avant de la passer au démonstrateur. Les algorithmes du raisonneur se basent sur les transformations qui préservent les propositions localement valides.
Les méthodes variationnelles d'assimilation des données sont très employées pour corriger les modèles numériques et particulièrement en géophysique. Ces méthodes utilisent un modèle direct (relation liant les variables géophysiques aux observations) qui décrit la physique du phénomène et confrontent les sorties de ce modèle avec des observations afin de déterminer (ou de corriger) les variables physiques qui les ont inférées. Le principe en est le suivant : déterminer le minimum d'une fonction de coût mesurant « l'écart » entre les observations et les sorties du modèle numérique, en faisant varier les paramètres du modèle physique (dits « paramètres de contrôle »). Cette méthode est très coûteuse sur le plan informatique, puisque qu'elle nécessite le calcule du gradient de cette fonction de coût par rapport aux variables de contrôle. D'autre part, plusieurs aspects algorithmiques se posent et qui sont liés aux différentes approches de modélisation proposées dans la littérature. Une nouvelle approche a été développée dans le cadre des laboratoires CEDRIC et LOCEAN, elle est basée sur la décomposition de systèmes complexes en graphes. Le formalisme modulaire permet la conception d'un outil général. En se basant sur ce formalisme, un prototype d'un outil logiciel intitulé YAO a été développé. Cet outil est un outil de modélisation et un générateur de code, il permet à l'utilisateur de se concentrer sur la spécification de son problème et de réduire sa part de programmation.
The Tableau Workbench (TWB) is a generic framework for building automated theorem provers for arbitrary propositional logics. The TWB has a small corethat defines its general architecture, some extra machinery to specify tableau-based provers and an abstraction language for expressing tableau rules.
This language allows users to ``cut and paste'' tableau rules from textbooksand to specify a search strategy for applying those rules in a systematic manner. A new logic module defined by a user is translated and compiled withthe proof engine to produce a specialized theorem prover for that logic. TheTWB provides various hooks for implementing blocking techniques using histories and variables, as well as hooks for utilising/defining optimisation techniques.
During this talk I will show how to build a theorem prover for few known modal logics starting from a pen and paper formulation, and if time permits, how to implement a more complex algorithm for the satisfiability of Computation Tree Logic (CTL).
Nous étudions des algorithmes concurrents en utilisant QUASAR un outil d'analyse et de validation de programmes concurrents.
Nous pensons que cet outil, en plus de son but initial de validation, peut être utilisé dans un aspect de génie logiciel pour fournir un indicateur global et une métrique de concurrence. Notre affirmation repose sur le fait que Quasar travaille sur le code source et s'appuie sur l'analogie avec une revue de code.
Avec Quasar nous avons un outil auquel on soumet un programme, qui (par slicing) en extrait la partie concurrente et qui (par model checking) essaie de le comprendre sous un certain point de vue lié à la concurrence des processus qui le composent. En particulier Quasar recherche des propriétés architecturales ou structurelles (symétries, structures simples, patterns) qui sont proches de celles qui sont conseillées pour obtenir de "bons" programmes. Il utilise les propriétés qu'il arrive à identifier, celles qui ne sont pas trop cachées par une programmation trop astucieuse, pour se faciliter la tâche et faire des réductions du nombre des cas à analyser. Nous avons commencé à utiliser la mesure de l'effort d'analyse que QUASAR doit faire sur la partie concurrente d'un programme pour qualifier ce programme sur le plan de la concurrence et nous pensons pouvoir en tirer une métrique donnant des indicateurs de génie logiciel pour le code concernant les aspects concurrents d'un programme.
Le séminaire s'appuiera sur le texte retenu à "13th International Conference on Reliable Software technologies" (2008) et sur la présentation Powerpoint que nous avons faites à la société Adacore (ancienne ACT Europe) qui a développé le compilateur Gnat en logiciel libre et qui travaille dans le domaine des logiciels et systèmes sûrs et dans le cadre du logiciel libre (Free Software Foundation). Ces documents sont en anglais, mais la présentation se fera en français.
D'autres éléments figurent sur le site QUASAR voir en particulier le tutorial et les publications sur l'utilisation de Quasar.
Nous présenterons l'architecture et les principes retenus pour le développement de notre outil QUASAR (ce n'est pas un exposé sur le model checking ni sur les réseaux de Petri), nous montrerons l'étude faite sur un algorithme de rendez-vous réparti utilisable dans une architecture pair à pair et les résultats de génie logiciel (comparaisons de solutions, de sémantiques de concurrence, facteur d'échelle, indéterminisme, qualité logicielle), nous rappellerons les autres études d'algorithmes concurrents faites en utilisant QUASAR et nous présenterons une liste d'extensions utiles pour Quasar.
Le slicing paraît être un point d'intérêt technique commun avec l'équipe CPR, aussi nous parlerons surtout des extensions utilisant le slicing.
Les réseaux de Petri sont un formalisme mathématique qui se prête particulièrement à la spécification et la modélisation des systèmes à événements discrets, ainsi au développement de systèmes distribués et concurrents. Ayant une sémantique comportementale, ils sont utilisés pour modéliser de manière non ambiguë la dynamique de toute spécification et description d'applications ou de systèmes. Mais avant toute chose ils permettent de simuler cette dynamique et surtout, par des techniques de vérification (model checking), de rechercher des propriétés comme l'inter-blocage, la vivacité, la famine, etc. Ils garantissent ainsi une meilleure fiabilité du produit à réaliser et assurent un gain d'effort significatif dans la réalisation de tels systèmes grâce à la réduction du nombre de tests de l'application qui est développée.
Les méthodes de vérification ne sont cependant efficaces que si elles sont implantées par des outils permettant l'automatisation du processus d'analyse et pouvant aussi assurer la génération automatique de code.
L'utilisation des réseaux de Petri pose néanmoins des difficultés pour la réalisation de systèmes de taille significative, car rapidement le concepteur d'application est confronté à l'explosion combinatoire des éléments à traiter. Les réseaux de haut niveau (HL nets) ont été définis pour résoudre ces problèmes en introduisant des concepts de haut niveau comme l'utilisation de structures de données complexes exprimées par exemple au moyen d'expressions algébriques.
Il faut aussi savoir qu'il existe différentes variantes et extensions des réseaux de Petri qui introduisent les notions de temps, de probabilités, etc.
On assiste ainsi à un foisonnement de modèles, outils et techniques. Plusieurs approches de recherche se complètent par conséquent. Afin d'obtenir une meilleure organisation des travaux au sein de la communauté internationale, une réflexion sur la normalisation du formalisme a démarré dans le milieu des années 1985 en vue de produire une BNF commune à tous les réseaux de Petri. Cette réflexion ne s'est concrétisée qu'en 2003 en soumettant à l'ISO un projet de standardisation, intitulé ISO/CEI 15909. Ce projet a pour objectif de permettre :
Nous présentons l'état d'avancement des travaux de normalisation. Ceux-ci font l'objet d'une coopération entre le lip6, le lipn, ainsi qu'avec les universités d'Adelaide (Australie) et Paderborn (Allemagne) sous la tutelle de l'ISO.
We consider the design of automated procedures for analyzing the (in)security of cryptographic protocols in the Dolev-Yao model for a bounded number of sessions when we take into account some algebraic properties satisfied by the operators involved in the protocol. This leads to a more realistic model than what we get under the perfect cryptography assumption, but it implies that protocol analysis deals with terms modulo some equational theory instead of terms in a free algebra.
The main goal of this paper is to set up a general approach that works for a whole class of so-called monoidal theories which contains many of the specific cases that have been considered so far in an ad-hoc way, e.g. exclusive or, Abelian groups, exclusive or in combination with the homomorphism axiom.
We follow a classical schema for cryptographic protocol analysis which proves first a locality result and then reduces the insecurity problem to a symbolic constraint solving problem. This approach strongly relies on the correspondence between a monoidal theory E and a semiring Se_E which we use to deal with the symbolic constraints. We show that the well-defined symbolic constraints that are generated by reasonable protocols can be solved provided that unification in the monoidal theory satisfies some additional properties. The resolution process boils down to solving particular quadratic Diophantine equations that are reduced to linear Diophantine equations, thanks to linear algebra results and the well-definedness of the problem. Examples of theories that do not satisfy our additional properties appear to be undecidable, which suggests that our characterization is reasonably tight.
This is joint work with Stéphanie Delaune, Pascal Lafourcade, and Denis Lugiez.
L'analyse morphologique des langues humaines consiste à analyser les formes textuelles élémentaires (lexème, forme morphologique, mot ou unité de ce genre) pour en extraire toute l'information possible, notamment les informations liées à la flexion (conjugaison, déclinaison, accord). Par exemple la forme "mangera" est analysée comme un futur indicatif 3e personne singulier du lemme "manger".
Un important courant de l'informatique linguistique utilise des machines finies pour décrire la morphologie des langues et construire des analyseurs. Le courant dominant utilise des règles de réécriture contextuelles compilées en transducteurs finis. L'opération essentielle est la composition de transducteurs.
Dans cet exposé, nous présentons et défendons une approche basée sur une sous-classe de transducteurs clos sous intersection. Cette opération est intéressante à bien des égards :
La restriction opérée sur le formalisme des transducteurs finis est compensée par une richesse d'opérations applicables : non seulement l'intersection, mais la différence ensembliste, la projection et la jointure relationnelle. Cela débouche sur un cadre où les transducteurs multi-bandes appartiennent à un univers unique quel que soit le nombre de bande (en particulier, les automates et les transducteurs ne sont plus de natures différentes) et où les opérations de l'algèbre relationnelle sont définies.
Constraint solvers are key modules in many systems, such as automated theorem provers, expert systems, and constraint logic programming environments. To efficiently or correctly incorporate constraint solvers in such systems, the capability of producing conflict sets or explanations of the results of the solvers is crucial. For example, conflict sets are useful to prune the search space of Satisfiability Modulo Theories (SMT) solvers, or to direct backtracking in CLP systems whereas explanations can be used to safely import the results of external reasoning modules in skeptical proof assistants.
For expressiveness, constraints are usually built out in unions of theories and constraint solvers in such unions are obtained by modularly combining solvers for the component theories. We briefly review the combination methods proposed by Nelson-Oppen, Shostak, and others. This rational reconstruction is the starting point for further investigations. We discuss the interest of using deduction complete satisfiability procedures and explanation graphs, which are capable of recording the entailment of some equalities. Using the notion of explanation graph, we give an abstract account of how to refine the Nelson-Oppen combination method to modularly build proof-producing satisfiability procedures.
Based on previous work on recursive function definitions, we aim to provide basic automation for formal termination proofs in Isabelle/HOL. We implemented two methods: The first one searches for lexicographic combinations of size measures. The second and more powerful one is based on the Size-Change Principle, whose soundness we have formalized in Isabelle. We show how these methods can be used to prove termination of recursive functions automatically, discuss their relative merits in practice, and possibilities for extending them or applying them in different contexts.
The general focus of my work - briefly sketched in this seminaire - is the application of interactive theorem proving in software engineering. I report in this talk on the analysis of the aspect-oriented paradigm and the calculus ASP for distributed objects. Although addressing different issues, both languages are built upon the sigma-calculus of Abadi and Cardelli. I present an outline of the formalization of the sigma-calculus in the theorem prover Isabelle/HOL that uses finite maps and de Bruijn indices and proves confluence and type safety.
Finally I sketch the next steps in the analysis of these two instances of the object-oriented paradigm and show up some possible future directions for the support of programming language analysis in specialized domains.
Nous présentons ici des travaux en cours visant à vérifier des propriétés de sécurité sur des programmes C. Dans ce contexte, nous décrivons une analyse de programmes C permettant de vérifier des propriétés de sécurité de type confidentialité, intégrité et authenticité, ainsi que le prototype qui la réalise. Au niveau théorique, cette analyse utilise principalement le cadre de l'interprétation abstraite, tandis qu'au niveau pratique le prototype s'appuie sur Frama-C, un cadre technologique en cours de développement au CEA LIST et facilitant la programmation d'analyses de programmes C.
Les outils de démonstration automatique de la terminaison (CiME, Talp, Aprove, TTT,...) sont devenus avec le temps de plus en plus efficaces et puissants. Cependant, pour parvenir à ces résultats, ces outils, bien que fondés sur des résultats théoriques solides, sont devenus très complexes (la taille du code de CiME est comparable celle du compilateur ocaml) et les preuves générées sont de plus en plus difficiles à vérifier "à la main". Le problème de la validité des preuves générées est dès lors posé.
Les assistants à la preuve (COQ, Isabelle/HOL,...) permettent quant à eux une grande confiance dans les preuves obtenues (grâce à un noyau restreint et facilement vérifiable) au prix d'un manque d'automatisation. En particulier, il n'existe pas (ou peu) d'aide en matière de preuve de terminaison.
Nous développons actuellement, dans le cadre du projet ANR A3PAT, une version de CiME fournissant une trace vérifiable dans un assistant à la preuve (actuellement Coq) des preuves de terminaison obtenues. À terme, cet outil permettra de générer automatiquement certaines preuves de terminaison dans les assistants à la preuve.
Nous présenterons notre démarche et notre prototype capable de certifier des preuves impliquant des critères complexes.
La complexité des logiciels ne cessant d'augmenter d'années en années, la vérification et la validation de tels systèmes deviennent des enjeux cruciaux, sur le plan économique avec l'accroissement des coûts de développement mais aussi sur le plan humain dans les cas d'applications critiques ou sensibles.
Parmi les techniques du génie logiciel permettant d'accroître la confiance dans le logiciel, nous nous intéressons aux méthodes formelles et plus particulièrement aux méthodes fondées sur la preuve et le raffinement.
Nous présentons trois approches que nous avons développées utilisant ces méthodes. Chaque approche est dédiée à un domaine d'application particulier : la modélisation géométrique à base topologique, les IHM, les composants logiciels. Au travers des résultats obtenus, nous montrons les possibilités qu'offrent les méthodes de ce type mais aussi certaines de leurs limites.
L'exposé présente un mécanisme d'invariants de représentation pour FoCaL offrant au programmeur la possibilité de décrire et de prouver des propriétés sur les données qu'il utilise pour représenter ses objets.
L'exemple d'une version certifiée de l'implantation des entiers modulaires et des corps finis de la librairie FoCaL actuelle nous permettra de dégager une implantation des structures quotient et un modèle d'invariants pour FoCaL
L'introduction de l'approche par composants dans la conception d'applications temps réel permet une plus grande compréhension, réutilisation et fiabilité du logiciel. Dans cet exposé nous présentons l'architecture à base de composants que nous avons définie pour faciliter la conception et l'analyse de ces systèmes. L'architecture est structurée en divers types de composants, notamment :
Afin de réutiliser efficacement les composants au sein de l'architecture nous avons défini plusieurs types de spécifications (appelées contrats) à associer aux composants. Ces contrats permettent de décrire les signatures et propriétés fonctionnelles des services offerts et requis des composants, leur dynamique ainsi que leurs propriétés temporelles. Lors de la phase d'assemblage, les contrats offerts et requis des composants sont négociés afin de déterminer si les contraintes d'utilisation des composants ne sont pas invalidées une fois qu'ils sont mis en relation.
Les formalismes utilisés permettent aussi d'effectuer d'autres types d'analyses sur l'ensemble d'un assemblage, comme la vérification des propriétés de sûreté et de vivacité et l'analyse d'ordonnançabilité.
Il s'agit d'un travail commun avec Christine Paulin (LRI, INRIA Futurs).
Nous présenterons Rml, un sous-ensemble du lambda-calcul simplement typé, enrichi avec quelques primitives probabilites. Un tel programme peut être vu comme une variable aléatoire, et donc représenter une mesure. Cela est rendu formel par le moyen d'une transformation monadique qui fait du programme un terme purement fonctionnel dans Coq, dénotant une mesure : opérationnellement un opérateur qui envoie une fonction mesurable à valeurs dans [0,1] dans [0,1] et logiquement possédant les bonnes propriétés pour être qualifiée de mesure.
Nous fournissons un cadre de raisonnement similaire à celui de la sémantique axiomatique de Hoare, qui ici consiste à se donner des moyens d'encadrer (minorer et majorer) une probabilité ou, plus généralement, une espérance mathématique. Notre cadre prend spécialement en compte des fonctions générales récursives qui définissent une probabilité, par exemple la loi géométrique. L'ensemble de ces outils s'appuie sur la contribution Coq de Christine Paulin, qui fournit une formalisation minimaliste des besoins en théorie de la mesure, sous la forme d'une axiomatisation de l'intervalle [0,1].
Nous proposons de développer cette approche à partir d'exemples concrets. Puis, en fonction du temps disponible, nous établirons les liens avec le langage LambdaO (Park, Pfenning, Thrun) ainsi que la transformation Call-by-Value qui donne le cadre pour étendre Rml à l'ensemble d'un lambda-calcul simplement typé et probabiliste.
Nous présenterons les travaux du projet Sardes sur la formalisation de Dream, une bibliothèque de composants permettant la construction d'intergiciels de communication, et le typage d'assemblages de composants Dream. Nous aborderons principalement la définition d'une sémantique pour un assemblage de composants Dream, centrée sur la manipulation de messages, ainsi que la description d'un système de types garantissant la sûreté de la manipulation des messages. L'objectif de cette présentation est de montrer les avantages apportés par un tel système de types, les difficultés rencontrées lors de la conception de ce système de types et l'approche pragmatique qui a finalement été choisie.
The dependency pair technique is a powerful method for termination proofs of first-order term rewrite systems (TRSs). We investigate how to extend and how to automate this technique. First, we show how to prove termination of higher-order functions. To this end, the dependency pair technique is extended to handle (untyped) applicative TRSs. Second, in a termination proof using dependency pairs one needs to find term orders that satisfy a given set of inequalities. One possibility is to search for orders that are generated by argument filters and lexicographic path orders. We present an encoding of this NP-complete search-problem into a satisfiability problem of propositional formulas that can be efficiently handled by SAT solvers. We implemented and evaluated our results in the automated termination prover AProVE. Extensive experiments show that by our extensions for higher-order functions one obtains increased termination proving power, and by the encoding and the application of SAT solvers one obtains speedups in orders of magnitude. Without these improvements AProVE would not be the winner of the "International Competition of Termination Tools" for TRSs in 2006.
La réalisation d'une preuve formelle dans un assistant à la preuve comme le système Coq comporte souvent une part de travail significative pour établir des résultats qui sont laissés implicites dans une preuve sur papier. Prouver la réalisation ou l'absurdité d'un jeu de contraintes (égalités/inégalités) polynomiales est un exemple représentatif de ce type de problèmes dont le contenu mathématique est faible mais dont le coût de la preuve formelle "à la main" peut s'avérer important.
Il est donc crucial pour la faisabilité de preuves variées et bien plus élaborées de fournir des outils d'automatisation adaptés pour décharger l'utilisateur de ce travail et lui permettre de se concentrer sur les étapes significatives de sa preuve. La terminaison de systèmes de réécriture, le théorème des nombres premiers ou la théorie des courbes elliptiques sont des exemples récents de telles applications. La situation est cependant très différente selon la structure algébrique qui sous-tend le système de polynômes étudié : selon les cas, on peut se trouver dans une théorie décidable et efficacement décidée (anneaux), décidable mais à coût très élevé (arithmétique réelle), voire indécidable (équations diophantiennes, inégalités entières).
Il s'agit ici de décrire les tactiques travaillant sur les systèmes d'égalités/inégalités récemment intégrés au système Coq et des perspectives de développement qui pourraient compléter cette boîte à outils.
Termination is one of the most interesting problems when dealing with context-sensitive rewrite systems. Although there is a good number of techniques for proving termination of context-sensitive rewriting (CSR), the dependency pair approach, one of the most powerful techniques for proving termination of rewriting, has not been investigated in connection with proofs of termination of CSR. In this talk, we show how to use dependency pairs in proofs of termination of CSR. The implementation and practical use of the developed techniques yield a novel and powerful framework which improves the current state-of-the-art of methods for proving termination of CSR.
Le développement modulaire est l'un des principaux avantages de la méthode B, malgré une sémantique mal définie ou trop éloignée de l'intuition par rapport à des langages plus usuels. Nous illustrons les différentes manières dont cette modularité a été étendue, ou redéfinie, dans diverses extensions de la méthode B. Nous mentionnerons notamment le problème de la modularité dans le cadre de la sémantique opérationnelle pour B (basée sur une logique temporelle) que nous avons proposée.
Lentement mais sûrement, l'industrie est en train de découvrir le besoin de langages de programmation, de plates-formes et de méthodologies appliquées à l'informatique distribuée. Malheureusement, à l'heure actuelle, toutes ces plates-formes -- industrielles ou académiques -- restent fragiles vis-à-vis de l'épuisement des ressources et proposent, au mieux, des solutions ad-hoc pour contrer certains accidents ou certaines attaques de déni de service.
Le langage Erlang, massivement utilisé dans les télécommunications, ne fait pas exception. Bien souvent, des agents malicieux programmés en Erlang ou en C pourront tromper un service honnête et le contraindre à allouer toute sa mémoire, utiliser toute son énergie, grignoter ses ramettes de papier, etc. C'est ce problème que nous examinerons, à l'aide d'outils sémantiques : comment définir un dépassement de ressources ? comment l'observer ? comment analyser un service et garantir -- si possible automatiquement -- que le système survivra à une attaque de Déni de Service ?
Pour répondre en partie à ces questions, nous parlerons de pi-calcul, de spécifications, de sémantique opérationnelle et de systèmes de types. Et peut-être un peu de code porteur de preuves.
Certains problèmes nécessitent des performances que seuls les machines massivement parallèles ou les méta-ordinateurs peuvent offrir. L'écriture d'algorithmes pour ce type de machines demeure plus difficile que pour celles strictement séquentielles et la conception de langages adaptés est un sujet de recherche actif nonobstant la fréquente utilisation de la programmation concurrente. En effet, la conception d'un langage de programmation est le résultat d'un compromis qui détermine l'équilibre entre les différentes qualités du langage telles que l'expressivité, la sûreté, la prédiction des performances, l'efficacité ou bien la simplicité de la sémantique.
Ce travail s'inscrivait dans le cadre du projet « CoordinAtion et Répartition des Applications Multiprocesseurs en objective camL » (CARAML) de l'ACI GRID dont l'objectif était le développement de bibliothèques pour le calcul haute-performance et globalisé autour du langage OCaml. Ce projet était organisé en trois phases successives : sûreté et opérations data-parallèles irrégulières mono-utilisateur ; opérations de multitraitement data-parallèle ; opérations globalisées pour la programmation de grilles de calcul.
Cet exposé est organisé en 3 parties correspondant chacune aux contributions de l'auteur dans chacune des phases du projet CARAML : une étude sémantique d'un langage fonctionnel (appelé BSML) pour la programmation BSP (Bulk-Synchronous Parallelism, un modèle qui permet la portabilité des programmes tout en offrant une prévision réaliste de leurs performances sur une grande variété d'architectures parallèles) et la certification des programmes écrits dans ce langage ; une présentation d'une primitive de composition parallèle (et qui permet aussi la programmation d'algorithmes « diviser pour régner » parallèles), un exemple d'application via l'utilisation et l'implantation de structures de données parallèles et une extension pour les entrées/sorties parallèles en BSML ; l'adaption du langage pour le méta-calcul.
Le développement actuel de l'utilisation des cartes à puces pour diverses applications critiques (cartes bancaires, cartes vitales, téléphonie mobile, ...) pose le problème crucial de la sécurité des plates-formes embarquées sur ces cartes. L'un des points centraux de cette sécurité est la vérification de bytecode permettant d'assurer la correction du code téléchargé sur les cartes à puces vis-à-vis d'un certain nombre de règles de sécurité (typage, non interférence, ...). Dans cet exposé nous présenterons une méthode et un outil de certification formelle de plates-formes mobiles, la boîte à outils JaKarTa.
Plus précisément, JaKarTa s'appuie sur la notion d'abstraction automatique de spécifications pour, partant de spécification "défensive" (effectuant à la fois les calculs et les tests de sécurité), aboutir à deux spécifications : une machine dite "offensive", n'effectuant plus de test de sécurité et donc plus efficace que la machine "défensive", et une machine dite "abstraite", n'effectuant plus que les tests de sécurité. Cette abstraction est validée de manière automatique par la production de preuves de correction en Coq. La machine abstraite peut, par la suite, être étendue en un "bytecode verifier" permettant d'effectuer une fois pour toutes de manière statique les tests de sécurité concernant une applet donnée lors de son téléchargement sur la carte à puce.
La technique employée pour la production des preuves de correction s'appuie sur la génération automatique en Coq de principes d'induction liés à une fonction que nous avons récemment renforcée.
Cet exposé présente la méthode de spécification EB3, conçue spécifiquement pour les systèmes d'information, et les techniques de synthèse (génération et interprétation de programmes) associées.
EB3 est une méthode formelle et exécutable, fondée sur le modèle entité-association, une algèbre de processus et une sémantique de traces. Elle permet de décrire complètement, de manière abstraite, le comportement attendu d'un système d'information, de sa base de données jusqu'à son interface graphique, incluant tout le traitement survenant entre les deux.
La synthèse automatique d'un système d'information à partir d'une spécification EB3 repose sur l'interprétation efficace d'une expression de processus et de fonctions récursives. Nous croyons que cette interprétation peut se faire en un temps comparable à celui d'une implémentation traditionnelle réalisée par un humain. Nous développons présentement un interpréteur pour EB3. Les résultats préliminaires obtenus avec cet interpréteur appuient cette hypothèse.
Nous présentons un interpréteur de traces de preuve en logique du premier ordre multi-sortée avec égalité.
Grâce à l'utilisation de la réflexion dans Coq, nous avons implanté cet interpréteur et prouvé formellement sa correction par rapport à l'interprétation réflexive des formules comme des propositions de Coq à l'intérieur-même de la théorie des types de Coq.
Ce cadre générique permet d'interpréter des traces de preuves calculées par n'importe quel prouveur automatique, pourvu qu'elles soient suffisamment précises : nous illustrons cela sur des traces de preuve produites par l'outil CiME lorsqu'il résout des problèmes d'unifiabilité grâce à la complétion ordonnée. Nous commentons les résultats obtenus sur la bibliothèque de problèmes TPTP.
Dans cet exposé, je présenterai les efforts d'adaptation à Coq des bibliothèques Ocaml de structures de données Set et Map. Ce travail a pour double objectif de garantir à l'utilisateur d'Ocaml la correction de ces bibliothèques Set et Map, et d'autre part de fournir à l'utilisateur de Coq des structures plus riches et efficaces que de simples listes.
Même si la partie concernant Set a été réalisée avec Jean-Christophe Filliâtre il y a bientôt trois ans, l'extension récente à Map avec Pierre Courtieu a donné lieu à une refonte en profondeur de cette bibliothèque Coq, avec en point de mire l'inclusion prochaine dans les théories standard de Coq. Je tenterai donc de décrire les points clés de ces travaux, tels que :
Wouldn't it be nice to be able to conveniently use ordinary real number expressions within proof assistants? In this talk, we outline how this can be done within a theorem proving framework. First, we formally establish upper and lower bounds for trigonometric and transcendental functions. Then, based on these bounds, we develop a rational interval arithmetic where real number calculations can be performed in an algebraic setting.
This pragmatic approach has been implemented as a setof strategies in PVS. The strategies provide a safe and convenient way to perform explicit calculations over real numbers in formal proofs.
Cet exposé présentera un aperçu des modèles de composants utilisés dans le cadre des intergiciels (middleware). Il fera le point et positionnera les modèles principaux (EJB, CCM, .Net/COM+, Fractal) les uns par rapport aux autres. L'accent sera mis sur le modèle Fractal et son écosystème. Nous présenterons également un aperçu des résultats obtenus au sein du projet Jacquard autour des composants et des aspects.
Le raffinement est une méthode pour dériver des programmes corrects à partir de spécifications. Un riche langage de types est un autre moyen d'assurer la correction des programmes. Nous proposons une extension de ML, conservative et à spectre large, en mélangeant ces deux approches.
Principalement, notre extension ajoute les types de base aux expressions, introduisant de ce fait du sous-déterminisme et des types dépendants. Nous ajoutons également une autre construction, appelée application démoniaque et duale de l'application usuelle du lambda calcul, de manière à augmenter la puissance du langage de spécification.
Nous présentons la sémantique de ce langage ainsi que son système de types. Donner un type aux expressions du langage est cependant indécidable. C'est la raison pour laquelle le système de types engendre des obligations de preuve garantissant la correction (partielle) des programmes.