Séminaire vérification de Toulouse

Ces travaux portent sur la certification de programmes impératifs. Les certificats établissent la validité des propriétés sémantiques des programmes et sont fournis sous forme depreuves déductives vérifiables par machine (http://en.wikipedia.org/wiki/Computer-assisted_proof). Le défi relevé est d'automatiser la construction des preuves de correction de programmes. Nous avons suivie l'approche de Floyd-Hoare pour prouver que les propriétés sémantiques sont des invariants du programme et nous avons utilisé le système Coq pour vérifier la validité des preuves.
On considère le cas où les propriétés sémantiques sont calculées par des analyseurs statiques (http://fr.wikipedia.org/wiki/Analyse_statique_de_programmes) de programmes qui s'appuient sur la théorie de l'Interprétation abstraite (http://www.di.ens.fr/%7Ecousot/publications.www/Cousot-TSI-00-Hermes-p155-164-2000.pdf). Nous proposons une méthode d'instrumentation des analyseurs statiques de programmes afin de leur faire générer automatiquement un certificat pour chaque propriété sémantique calculée. L'instrumentation consiste à associer à certaines fonctions d'un analyseur statique des patrons de preuve qui à l'exécution généreront les certificats. De tels analyseurs instrumentés ne sont pas pour autant certifiés puisque leur correction pour toutes leurs entrées possibles n'est pas garantie, néanmoins ils sont capables de justifier par une preuve formelle la correction du résultat de chacun de leurs calculs. Bien sûr, si pour une entrée possible l'exécution de l'analyseur est boguée le résultat sera erroné et la justification produite ne sera pas une preuve valide; elle sera rejettée par le vérificateur de preuves (Coq dans notre cas).
Cette approche permet de certifier avec un très haut-niveau de confiance (celui du vérificateur de preuves) les résultats d'outils existants, même à l'état de prototypes. Pour que l'instrumentation soit applicable en pratique, nous avons cherché à limiter le nombre de fonctions à instrumenter. Nous avons dégagé un ensemble restreint de fonctions, commun à tout analyseur, à instrumenter pour qu'un analyseur existant devienne un outil de certification automatique.
Nous avons appliqué cette technique d'instrumentation à un analyseur de programmes manipulant des tableaux (http://mathias.xn--pron-bpa.eu/index.php?menu=2,0,10#pldi08) qui s'appuie sur des domaines abstraits non triviaux. Cet analyseur calcule des propriétés sur le contenu des tableaux manipulés par les programmes et, grâce à notre instrumentation, génère désormais des certificats vérifiables par Coq attestant de la validité des propriétés découvertes par l'analyse statique.

Establishing adequacy of implementations of software transactional memory (STM) is notoriously non-trivial. Above all, it is difficult to determine the desirable notion of correctness and to define it mathematically. But describing an implementation of STM in a form amenable to mathematical scrutiny and proving it correct with respect to the chosen notion of correctness are also subtle and error-prone tasks. In this talk, I describe an experiment in this direction. We defined a particular STM implementation for the While language with parallelism and nested transactions in terms of a transactional small-step semantics, stated Guerraoui and Kapalka's opacity for this implementation in terms of simulability of runs in the transactional semantics by runs in a sequential semantics and vice versa for a suitable notion of agreement between configurations in the two semantics, and proved that it holds. We formalized the whole development in the dependently typed programming language Agda. (Joint work with Andri Saar.)

Avec le projet PROSEU, contrat DGE faisant en principe collaborer laboratoires et industriels français et québécois, nous avons été amenés à nous intéresser à quelque chose qui nous préoccupait moyennement jusqu'à présent (mais un vrai problème, identifié à la fin des années 70): les erreurs transitoires [alias erreurs « soft », alias SEU (Single Event Upsets)], leurs causes, leurs effets, particulièrement dans les systèmes embarqués, et comment s'en protéger avec le meilleur rapport qualité/prix.
C'est à un résumé de notre activité sur ce sujet que sera consacré l'exposé: ce qu'on sait faire actuellement et les idées que nous nous proposons de mettre en oeuvre

Le lambda calcul non typé, créé en 1936 par Alonzo Church, est une théorie très largement utilisée en logique, théorie des types, programmation fonctionnelle, linguistique, etc...
Le théorème de Church-Rosser en particulier fait partie de ses résultats les plus importants et les plus utilisés. Son énoncé est le suivant :
Theorem 1.32 (Church-Rosser theorem for ▹ß)
If P ▹ß M and P ▹ß N, then there exists a term T such that M ▹ß T and N ▹ß T
La plupart des preuves du théorème de Church-Rosser ne prennent pas vraiment en compte les problèmes liés à l'⍺-conversion, le renommage de variables liées au sein d'un terme. Elles définissent en général des classes d'équivalence pour la relation d'⍺-conversion ce qui leur permet de s'affranchir des difficultés naissant du renommage et de la substitution des variables liées. Certains trouvent cela dommage car l'⍺-conversion est une relation extrêmement importante en lambda calcul.
J. Roger Hindley et Jonathan P. Seldin proposent dans leur livre Lambda Calculus and Combinators, an Introduction une preuve gardant l'⍺-conversion du début à la fin. L'idée est de définir une conversion alternative appelée ⍺0-conversion, équivalente à l'⍺-conversion, mais qui leur permet de traiter la substitution plus simplement.
Cependant, lors de sa rencontre avec Makoto Tatsuta le 24 Mai 2010, Hindley lui avoua qu'il n'etait pas certain de l'exactitude de sa preuve. C'est la raison pour laquelle nous nous sommes lancés dans une verification sous Coq, un assistant de preuve développé en collaboration entre l'INRIA, école Polytechnique, Université Paris-Sud 11 et le CNRS, de la preuve de son livre. Notre but était d'avancer le plus possible dans la verification, la durée de mon séjour au NII étant limité.
Avec l'aide de Makoto Tatsuta et de Xavier Thirioux, j'ai tout d'abord défini la structure de notre lambda calcul et prouvé quelques résultats basi- ques sur celle-ci, puis implémenté la substitution de variables accompagnée de quelques autres résultats, pour finir par l'⍺-conversion et ses lemmes nécessaires à la preuve elle-même.

Parmi les outils de vérification utilisés aujourd'hui, les interprètes abstraits jouent un rôle de plus en plus important. Ils reposent sur un représentation abstraite des propriétés des logiciels, les domaines abstraits. Que ce soit dans les cadres industriels critiques où l'on veut avoir confiance dans ces outils, ou dans l'enseignement où l'on veut pouvoir synthétiser totalement ou partiellement des analyseurs pour faire intervenir les élèves, la génération automatique de domaines abstraits finis prend tout son sens. Nous présentons ici notre approche qui génère un domaine abstrait et ses fonctions de transfert sémantique à partir d'une description de la structure de son treillis et d'une fonction de concrétisation. Cette méthode repose sur Camlp4 pour construire un module Caml de type "domaine abstrait" et sur des solveurs SMT pour calculer au mieux les opérations de transfert du domaine.

Data flow languages are high level programming languages commonly used in industry to model and implement reactive embedded systems controlling a vast variety of devices.
We present a general approach for proving automatically safety properties of data flow programs. The approach extends and combines Model Checking with Satisfiability Modulo Theories (SMT) techniques. In it, a given program and property are first translated into formulas belonging to a decidable fragment of first-order logic that includes the combined theory of the program's data types--such as integers, reals, Booleans and so on. Then the property is proved by induction over the length of program executions using as reasoning engine an SMT solver specialized on that theory.
This talk will provide a high level description of the basic approach and its main enhancements as applied to the data flow language Lustre. Among the enhancements, it will then focus on a novel invariant discovery mechanism used by the model checker to strengthen its inductive reasoning steps and increase its success rate in proving safety properties.

Dr. Cesare Tinelli is an associate professor of Computer Science at the University of Iowa. He received a PhD in Computer Science from the University of Illinois at Urbana-Champaign in 1999. His research interests include automated reasoning, formal methods, foundations of programming languages, and applications of logic in computer science.
He is a founder and leader of the SMT-LIB initiative, an international effort aimed at standardizing benchmarks and I/O formats for Satisfiability Modulo Theories solvers. He received an NSF CAREER award in 2003 for a project on improving extended static checking of software by means of advanced automated reasoning techniques, and a Haifa Verification Conference award in 2010 his role in building and promoting the SMT community. He has given invited talks at such conferences as CAV, HVC, TABLEAUX, VERIFY, and WoLLIC.
His research has been funded by the US National Science Foundation, the US Air Force Office of Scientific Research and Intel Corp., and has appeared in more than 40 refereed publications, including articles in such journal as Artificial Intelligence, Information and Computation, the Journal of the ACM, Logical Methods in Computer Science, and Theoretical Computer Science.
He is a founder of the SMT workshop and has served in the program committee of numerous automated reasoning conferences and workshops, and in the steering committee of CADE, IJCAR, FTP, FroCoS and SMT. He will be the PC chair of FroCoS'11. He is also an associate editor of the Journal of Automated Reasoning.

Les systèmes réactifs deviennent extrêmement complexes avec l’essor des hautes technologies. Malgré les progrès techniques, la grande taille de ces systèmes facilite l’introduction d’une plus grande gamme d’erreurs. Parmi ces systèmes, les systèmes asynchrones, composés de sous-systèmes communiquant par échange de messages via des files d’attentes (par exemples des protocoles, des systèmes de communication bord/sol. . . ), apportent une complexité encore supérieure.
Actuellement, les industries engagent tous leurs efforts dans le processus de tests et de simulations à des fins de certification. Néanmoins, ces techniques deviennent rapidement inexploitables pour débusquer des erreurs pouvant conduire à des situations catastrophiques. La couverture des jeux de tests s’amincit au fur et à mesure de la complexification des systèmes, et il devient nécessaire d’utiliser de nouvelles méthodes. Parmi celles-ci, les méthodes formelles ont contribué, depuis plusieurs années, à l’apport de solutions rigoureuses et puissantes pour aider les concepteurs à produire des systèmes non défaillants. Dans ce domaine, les techniques de model-checking ont été fortement popularisées grâce à leur faculté d’exécuter, plus ou moins automatiquement, des preuves de propriétés sur des modèles logiciels.
Néanmoins, cette méthode souffre du problème de l’explosion combinatoire. Pour contrer ce phénomène, les méthodes de réduction par ordres-partiels se sont révélées particulièrement efficaces pour éliminer à la volée des séquences de transitions équivalentes de l’automaten global, là où le model checking classique effectuait un parcours exhaustif.
Toutefois, les travaux sur les ordres-partiels issus de la littérature appliquent les méthodes de réduction, lors de la construction de l’automate global composé du système, de son environnement complet ainsi que de la propriété à vérifier. Or, dans la majorité des cas, les propriétés à vérifier correspondent à des cas d’utilisation bien spécifiques et par conséquent la prise en compte de l’environnement complet du système n’est pas nécessaire.
L’approche dans laquelle s’insère ce travail, prend un point de vue complémentaire en considérant la réduction, non plus du système global, mais plutôt de son environnement. En effet, l’idée est d’abord de réduire les comportements du système en décrivant un cas d’utilisation particulier de l’environnement avec lequel le système interagit. L’objectif est de guider le model-checker à concentrer ses efforts, non plus sur l’exploration de l’automate global, mais sur une restriction pertinente de ce dernier pour la vérification. Pour cela, l’environnement (appelé contexte) est déplié et partitionné pour générer un ensemble de scénarios. La vérification effective s’effectue ainsi en composant chaque scénario avec le système et la propriété à vérifier. Sur cette idée, une méthode de description de l’environnement appelée contexte a été développée, pour permettre à l’utilisateur de spécifier, dans un langage simple, le comportement souhaité de son environnement. La description de l’environnement et la décomposition de la vérification, en vérification élémentaire sur chaque scénario, apporte une réduction importante de l’explosion combinatoire en espace.
Néanmoins, dès lors que le nombre d’acteurs (c’est à dire des éléments parallèles ou acteurs de l’environnement) devient important, le nombre de scénarios dépliés peut devenir prohibitif (par exemple, un environnement composé de P acteurs concurrents chacun émettant un message au système, générera P ! scénarios), et par conséquent une explosion combinatoire en temps et non plus en espace. La complexité du processus de vérification n’a pas disparue mais a seulement changé de nature. L’explosion combinatoire qui était de nature spatiale devient, par cette méthode, de nature temporelle.
Pour contrer cette explosion temporelle, nous proposons d’étendre les méthodes de réduction d’ordres partiels et la théorie des traces de Mazurkiewicz de manière à déterminer une équivalence entre les scénarios du contexte afin de supprimer ceux qui ont le même impact sur le système. Nous appliquons la méthode sur des modèles SDL, tout d’abord dans le cas mono processus puis dans le cas multi-processus sur deux cas d’études avioniques industriels. Nous comparons les résultats avec un model-checker performant : SPIN.

Dans cette présentation, nous examinerons les fondements d'une théorie de la conception d'un système embarqué par contrats, à partir d'un ensemble de considérations méthodologiques. Après avoir passé en revue différentes tentatives pour satisfaire ces fondements, nous étudierons les contrats modaux, unification des automates d'interface de de Alfaro/Henzinger et des spécification modales de Larsen, qui offrent toute la flexibilité espérée et supportent, en particulier, le raisonnement compositionnel avec une complexité algorithmique satisfaisante.

Shared decision diagram representations of a state-space have been shown to provide efficient solutions for model-checking of large systems. However, decision diagram manipulation is tricky, as the construction procedure is liable to produce intractable intermediate structures (a.k.a peak effect). The definition of the so-called saturation method has empirically been shown to mostly avoid this peak effect, and allows verification of much larger systems. However, applying this algorithm currently requires deep knowledge of the decision diagram data-structures, of the model or formalism manipulated, and a level of interaction that is not offered by the API of public DD packages.
Hierarchical Set Decision Diagrams (SDD) are decision diagrams in which arcs of the structure are labeled with sets, themselves stored as SDD. This data structure offers an elegant and very efficient way of encoding structured specifications using decision diagram technology. It also offers, through the concept of inductive homomorphisms, unprecedented freedom to the user when defining the transition relation. Finally, with very limited user input, the SDD library is able to optimize evaluation of a transition relation to produce a saturation effect at runtime. We further show that using recursive folding, SDD are able to offer solutions in logarithmic complexity with respect to other DD. We conclude with some performances on well known examples.

Les technologies omniprésentes dans notre environnement intègrent désormais des éléments logiciels facilitant leur utilisation. Ces technologies offrent un vaste laboratoire d’expérimentation pour la recherche et en particulier pour l’informatique appliquée; elles sont un support évident pour rendre des services aux personnes dans leur vie quotidienne. Ces services concernent divers champs d’applications, chacun servant des objectifs spécifiques : confort, sécurité, accès à l’information ou encore assistance à la personne. Puisque les applications offrant ces services sont intimement liées aux besoins des utilisateurs, il est indispensable qu’elles s’adaptent facilement à leurs besoins. Une manière de répondre à ce défi est de proposer à l’utilisateur des outils pour programmer lui-même ses applications. Notre contribution consiste non seulement à définir un tel outil, sous la forme d’un langage visuel paramétré par un champ d’applications, mais aussi à proposer une méthodologie dont l’objectif est de guider un utilisateur dans la programmation d’applications à l’aide de ce langage. Cette méthodologie est dédiée à l’orchestration d’entités communicantes : elles représentent les technologies déployées dans nos environnements. Notre approche, associant une méthodologie à un langage, est accessible à un programmeur novice et suffisamment expressive pour traiter divers champs d’applications. Afin d’augmenter la confiance de l’utilisateur dans le développement de ses applications, nous étendons la méthodologie en proposant une approche de développement dirigée par la vérification de quelques propriétés. Cette vérification est permise par la sémantique du langage, formellement définie.
Mots clés : méthodologie, langages visuels, langages dédiés, accessibilité, assistance à la personne

One of the primary purposes of embedded software and systems is to implement control algorithms aimed at harnessing the dynamics of complex dynamical systems, such as aircraft, automobiles, fast trains and automated transit systems. The necessity to certify these systems makes it a requirement to extract the semantics of the software as it interacts with the physical world. Several tools exist to achieve that goal, and they have displayed excellent performance when applied to large safety-critical software such as that present in avionics systems.
This presentation will be devoted to the contributions that control theory may bring to the extraction of useful control software semantics. It will be shown by means of examples that the process by which such semantics is obtained may be greatly simplified when working with control system specifications first. Numerical issues that arise when moving from the ideal world of system specifications to the concrete software environment will also be discussed. i

First working day on time-oriented embedded systems will be held on November 2, 2010, at ENSEEIHT, Toulouse. Expected invited speakers are Edward A. Lee (U. of California at Berkeley, USA), Wolfgang Pree (U. of Salzburg, Austria) and Jean-Pierre Talpin (IRISA, Rennes, France). All information at http://www.irit.fr/torrents/activities.php.

The Development Assurance Level (DAL) indicates the level of rigor of the development of a software or hardware function of an aircraft. The DAL (ranging from E to A) guides the assurance activities that should be applied at each stage of development. These activities aims at eliminating design and coding errors that would have a safety effect on the aircraft.
The new standard ARP4754a has established rules to allocate the DAL to functions. The allocation is primarly based on the severity of the effects of a function implementation error. But new rules introduce the possibility to downgrade the DAL levels based on various notions of independence (requirement, implementation, execution independence). In the context of the MISSA project we investigate means to assist the safety specialists when checking an existing DAL allocation or generating an allocation.
In this talk we will present our work on the formalization of the DAL allocation rules and its implementation using a pseudo-boolean solver. We will illustrate the talk with various critical aircraft systems including the Electrical Generation and Distribution System.

Model-checking consists in building a formal model of a program, and prove its correctness by checking that the state-space of the model does not contain any bad state. Most programs have infinite state-spaces that must be entirely explored by model-checking algorithms to ensure correctness. This is particularly the case for real-time systems, due to the continuous nature of time.This entails two main problems: the finite representation and the effective computation of infinite sets of states. We present a technique based on Real Vector Automata (RVA) for the representation of state-sets and on acceleration to help the termination of state-space exploration. RVA are weak Büchi automata that we use to encode sets of values definable in Presburger arithmetic over reals and integers. They can particularly represent infinite periodic unions of sets, that we use in turn to capture loop invariants in the model. We show that we can express the iteration of any loop in a timed automaton as a Presburger formula. Following a result of Comon & Jurski on the flatness of timed automata, this yields an algorithm for the computation of the reachability space of timed automata. For linear hybrid automata, we present a technique to compute invariants for ultimately periodic loops. Despite model-checking linear hybrid automata is undecidable, our approach succeeded on many examples found in the literature.

We describe an algebra of Edge-Valued Decision Diagrams (EVMDDs) to encode arithmetic functions and its implementation in a model checking library.
We provide efficient algorithms for manipulating EVMDDs and review the theoretical time complexity of these algorithms for all basic arithmetic and relational operators. We also demonstrate that the time complexity of the generic recursive algorithm for applying a binary operator on EVMDDs is no worse than that of Multi-Terminal Decision Diagrams.
We have implemented a new symbolic model checker with the intention to represent in one formalism the best techniques available at the moment across a spectrum of existing tools.
Compared to the CUDD package, our tool is several orders of magnitude faster.

L'exposé présente une méthode de vérification d'algorithmes manipulant des graphes à l'aide de leur représentation sous la forme d'arbres couvrants décorés de pointeurs additionnels. Nous illustrons ce concept par la vérification d'une version (pseudo-)impérative de l'algorithme de Schorr-Waite, par raffinement d'une version fonctionnelle manipulant des arbres. Ce développement se compose de deux étapes indépendantes:

• le raffinement de l'algorithme fonctionnel en une version impérative, démontré par simulation
• la correction de la version fonctionnelle lors de l'ajout de pointeurs aux arbres qui sont finalement fusionnées pour obtenir le résultat. De plus, les spécifications impératives utilisent des monades et du sucre syntaxique les rendant très proches d'un programme impératif classique
  L'ensemble du travail a été réalisé dans l'assistant de preuve Isabelle/HOL.

Cet exposé présentera les principes de génération de code à partir de modèles AADL, et les fonctionnalités couvertes par Ocarina notre générateur de code. Ocarina est un projet joint entre Télécom ParisTech, l'ISAE et l'ENIS.
AADL est un langage de description d'architectures normalisé par la SAE. La version 2 du langage a été publiée en Janvier 2009. La conception de ce langage vise à fournir les briques de base pour exprimer les éléments fondamentaux de l'architecture en vue de l'analyser. Parallèlement à ces activités, AADL permet aussi de générer de nombreux éléments (tâches, tampons et canaux de communications, tables de routages ..). Tirant partie des informations architecturales, il est possible de générer un code compact, optimisé et conforme aux exigences strictes de qualité de code (Profil Ravenscar et Haute-Intégrité de Ada, ECSS-40 de l'ESA et recommandations liées au langage C). Afin de supporter cette génération de code, Nous avons étendu AADLv2 et dirigé la direction de trois documents annexes clarifiant les patrons de modélisation à utiliser pour garantir que l'on est en mesure de générer du code.
Ocarina est un outil de génération de code basé sur AADL. Il génère du code Ada, C ou Real-Time Java. Le code généré peut s'exécuter aussi bien sur des plates-formes natives qu'embarquées (RTEMS, bare-board, RT-Linux). De plus, il couvre aussi bien des systèmes basés sur RT-POSIX, que des systèmes partitionnés se fondant sur les concept de ARINC653. Il a été validé au travers de plusieurs cas d'étude avec l'ESA, Thales et leurs partenaires.

Un graphe attribué est constitué d'une partie structurelle, et d'attributs qui sont associés aux éléments de la structure. Pour réaliser des transformations de graphes attribués, il faut donc transformer la structure, et réaliser des calculs sur les attributs.
En ce qui concerne la transformation structurelle, il existe deux approches principales: le double pushout et le simple pushout.
Au niveau du calcul sur les attributs, Ehrig a enrichi l'approche double pushout à l'aide d'attributs définis dans le cadre de la théorie des types algébriques. L'approche développée par Ehrig, nécessite de créer des sommets en fonction du nombre de valeurs possibles pour un calcul, ce qui fait que l'implémentation du calcul sur les attributs pose problème et se fait en dehors du cadre formel développé dans sa théorie.
L'approche DPoPb (Double Pushout, Pullback), développée dans la thèse de Maxime Rebout offre un cadre théorique unique qui contient la réécriture de la partie structurelle des graphes et les calculs sur les attributs du graphe. Les espaces des attributs sont des types inductifs, et le calcul sur les attributs se fait à l'aide de moyens qui sont assurés par la théorie des types inductifs. En plus d'avoir un formalisme unique pour la transformation de la structure et des attributs, la puissance de calcul des types inductifs est supérieure à celle des types algébriques car on peut avoir des fonctions comme arguments.
Nos travaux actuels se concentrent sur le calcul sur les attributs: nous étudions comment traiter le calcul des attributs à l'aide des types inductifs, également dans l'approche simple pushout pour comparer avec l'autre approche (Double Pushout) que nous avons déjà étudiée.
De plus, les types inductifs permettent de représenter l'infini d'une certaine manière (par exemple des arbres aux branchements infinis). Il est également possible de faire passer de l'information des attributs, à la structure du graphe. Ce qui nous donne une piste pour représenter un graphe dont la structure a une taille infinie.
La dernière partie de l'exposé est consacrée au côté algorithmique et aux questions d'implémentation de réécriture de graphes par l'approche DPoPb.

L'exposé passe en revue les différentes méthodes de vérification modèle checking borné et non borné basées SAT/SMT ayant diffusé avec succès dans l'industrie dans les années récentes (induction, interpolation), et introduit quelques unes des tendances futures.

Le model checking utilise l'équivalence entre la définissabilité d'un langage de mots par une formule de la logique monadique du deuxième ordre (MSOL) et sa reconnaissabilité par un automate fini ("Théorème de Buchi").
Cette logique permet d'exprimer la plupart des logiques temporelles usuelles. Les applications d'aujourd'hui étant principalement distribuées, on voit l'utilité de caractériser MSOL pour des langages d'ordres partiels étiquetés (LPO), qui sont un modèle plus expressif et fidèle de leurs comportements. Des propriétés analogues au theorème de Buchi ont été prouvées pour des classes restreintes de LPO, telles que les traces de Mazurkiewicz ou les MSC (qui sont la version formelle des diagrammes de séquences d'UML).
Dans cette présentation, nous considérons les systèmes de transition par pas avec autoconcurrence (Step Transition Systems), et définissons une sémantique par langages de LPO qui constitue une extention des sémantiques concurrentes usuelles des Réseaux de Petri. Nous mettons en évidence plusieurs caractérisations de la définissabilité par MSOL de ces langages en termes de régularité, caractérisations qui étendent nombre des résultats mentionnés ci-dessus.
Nous montrons comment ces résultats s'appliquent en particuliers aux langages concurrents des réseaux de Petri.
(travail commun avec Rémi Morin du Lif, en partie publié à PN 2009)

This talk, to be held in english, will get into the g(l)ory details of MLF: introducing MLF new types, their interpretation, the type instance relation, typing rules, type-inference algorithm, unification algorithm, and so on, as long as the audience can bear it.

Les logiques de description (LD) forment une famille de langages adaptés pour la représentation et le raisonnement sur des connaissances d'un domaine d'application d'une façon structurée et formelle. Les outils de représentation et de raisonnement sur des connaissances est actuellement l'un des champs d'application des méthodes formelles, dont l'objectif est d'assurer leur fiabilité. Un point essentiel de l'application de ces méthodes formelles est la preuve de validité des raisonnements dans des LDs, comme celle de la terminaison, l'adéquation (soundness) et la complétude d'un raisonneur. Dans cet exposé , on présente une spécification formelle de la syntaxe et de la sémantique de ALC, qui est considérée comme un représentant typique d'une large gamme de LDs. On prouve pour cette logique les propriétés d'adéquation, de complétude et de terminaison dans l'assistant de preuve Coq.

The talk generalises a famous result from game theory. It presents one proof and sketches three alternative ones.
In a game from game theory, a Nash equilibrium (NE) is a combination of one strategy per agent such that no agent can increase his payoff by unilaterally changing his strategy. Kuhn proved that all (tree-like) sequential games have NE. Osborne and Rubinstein abstracted over these games and Kuhn's result: they proved a *sufficient* condition on agent *preferences* for all games to have NE. I will present a *necessary and sufficient* condition, thus accounting for the game-theoretic frameworks that were left aside. The proof is *formalised* using Coq, and contrary to usual game theory it adopts an inductive approach to trees for definitions and proofs. By rephrasing a few game-theoretic concepts, by ignoring useless ones, and by characterising the proof-theoretic strength of Kuhn's/Osborne and Rubinstein's development, the talk also intends to clarifies sequential game theory.
Then I will sketch an alternative proof. Both proofs so far pre-process the preferences by topological sorting, which is surprising since it decreases the number of NE. Finally I will sketch two other proofs that pre-process the preferences only by transitive closure. The four proofs are all constructive and by induction, and I will compare them when seen as algorithms. The four proofs also constitute diverse viewpoints on the same concepts, the trial of diverse techniques against the same problem, and reusable techniques for similar structures.

For the call-by-name restriction of Curien and Herbelin's lambda-bar-mu-mu-tilde calculus - a calculus for the study of the computational behaviour of classical proofs, an alternative proof of termination of all computations is given in a very syntactic (and hence elementary) way, namely by simulation of all steps in simply-typed lambda calculus. First, the calculus is embedded into a new monadic extension of Parigot's lambda-mu calculus by way of a monadic translation. The new calculus is in turn embedded into simply-typed lambda calculus by a CPS (continuation-passing style) translation. This is joint work with Espírito Santo and Pinto in Braga (Portugal).

Type systems are designed to guarantee that typable programs are safely executed. Therefore it is expected that we can automatically check whether a program is typable or not, and such a problem is called type-inference problem (or typability problem) of type systems. The type-checking problem is another type-related problem: does a program have a given type or not? The type inference is known to be decidable in both the simply-typed lambda calculus and the type system of ML, and the problems in the impredicative polymorphic lambda calculi have been studied. On the other hand, the problems for existential types have not been studied enough. In this talk, some recent results on type-related problems for polymorphic and existential types are presented. In particular, the undecidability for the domain-free lambda calculus with existential types, which was proved by the speaker, is presented. The proof gives a new theoretical application of the continuation-passing-style (CPS) translations.

This presentation comes as a positive reaction inspired by Ralph Matthes' presentation of May, 19. This notably dealt with termination proofs for the simply-typed lambda-calculus augmented with new reduction rules. My presentation will sum up results published in Mathematical Structures in Computer Science, Volume 18, Special Issue 04, August 2008.
A common way to show the termination of the union of two abstract reduction systems, provided both systems terminate, is to prove they enjoy a specific property (some sort of “commutation” for instance). This specific property is actually used to show that, for the union not to terminate, one out of both systems must itself be non-terminating, which leads to a contradiction. One nice feature of such a proof technique is that it often relies on simple diagram chasing.
Sometimes, however, these proofs will not work because there are some cases where the objects (whatever they may be: terms, trees, graphs, or so) are too complex for the diagrams to be closed. On the other hand, there are situations such that if the object at the root of the diagram satisfied some condition, the diagram in question could be closed.
Thus, I will define an operator transforming an infinite reduction sequence into another one by inserting a given reduction step at the beginning of the sequence. Then I will give an example of how it may be used to derive a new lemma ensuring that the union of two reduction systems is terminating. Finally, I will apply this lemma to two case studies.

Les langages de programmation comme OCaml et Haskell reposent sur des règles de typage garantissant la bonne exécution des programmes. En pratique, le typage permet de détecter maintes erreurs de programmation à la compilation. Depuis vingt ans, de nombreux travaux visent à enrichir ces sytèmes de types avec le polymorphisme de première classe (i.e. en ajoutant le quantificateur universel "pour tout"). Le référentiel pour le polymorphisme a été défini en 1972 dans le domaine de la logique : c'est le Système F (Girard). Mais en pratique, le Système F est inutilisable comme langage de programmation, à la différence de OCaml ou Haskell. De plus, l'adaptation naïve du Système F à ces langages rend le typage indécidable.
Dans cet exposé, nous détaillons intuitivement le problème en expliquant pourquoi les solutions proposées jusqu'à présent ne sont pas satisfaisantes. Nous présentons ensuite MLF, un système de types qui répond aux exigences posées, puis nous illustrons avec des graphes l'algorithme d'unification de MLF.

Nous présentons tout d'abord le projet CAVALE (Combinaison d'Analyses pour la VALidation de Logiciels Embarqués). Cette composition doit permettre d'obtenir une meilleure connaissance du système que chacune des analyses prises séparément.
Ce projet a pour objectif:
1) de proposer un cadre permettant la composition d'analyses statiques, (interprétation abstraite, méthode déductive, ...) et de techniques de test dynamique (méthode de construction, critère de couverture, ...) pour un programme C embarqué, découpé en lots fonctionnels ;
2) de réaliser un prototype s'intégrant dans la plateforme Frama-C.
Puis nous présentons un état de l'art des travaux récents dans le domaine, ainsi que nos propres pistes de réflexion, permettant la composition d'analyses avant ou arrière, symboliques (exactes) ou approchées, par plus petits ou plus grands points fixes le cas échéant.

Cet exposé rappelle la traduction CPS pour le lambda-calcul simplement typé et son intérêt, la comparaison avec la variante "colon translation" de Plotkin et sa généralisation aux monades par Wadler. Une variante "continuation-and-garbage-passing style" par Ikeda et Nakazawa est étudiée pour le cas d'un lambda-calcul avec application généralisée qui illustre les problèmes de calculs pour la recherche de preuves. La troisième partie montre une extension vers un calcul de la logique classique de Curien et Herbelin pour lequel une simulation dans le lambda-calcul simplement typé est obtenu par une traduction monadique vers une nouvelle extension monadique du lambda-mu-calcul de Parigot, suivi par une traduction CPS. Tous les résultats qui ne sont pas "classiques" ont été obtenus en collaboration avec Espírito Santo et Pinto à Braga en Portugal depuis octobre 2006.

Coccinelle est un outil qui permet de faire de la reconnaissance de motifs et de la transformation sur du code C. Développé à l'origine pour pallier le problème de l'évolution collatérale dans les pilotes du noyau linux, il est aussi utilisé pour détecter et corriger des bugs. Les motifs à reconnaître sont traduits en formules de logique temporelle, et interprétés sur le graphe de flot de contrôle du programme C. La reconnaissance de motifs correspond alors à la détection des noeuds du graphe de flot de contrôle qui satisfont la formule correspondante (par un algorithme de model checking).
Nous présenterons le langage qui permet de spécifier les motifs et les transformations de code, ainsi que la logique temporelle sous-jacente.

Nous décrivons la formalisation d'un langage synchrone (du style de Signal) dans l'assistant de preuve Isabelle. Dans cet exposé, nous nous intéressons au calcul d'horloge et à la question de "type soundness" de ce langage. Les langages synchrones sont basés sur l'hypothèse que les calculs d'un programme synchrone sont exécutés à des instants spécifiques, comme déterminé par les horloges des signaux manipulés par le programme. Un système de type d'horloge doit assurer que le programme ne traite pas de données invalides. Dans l'exposé,

• nous décrivons un système de types, qui est essentiellement un système d'équations ensemblistes
• nous montrons un résultat de "type soundness" qui assure que, si le système d'équations dérivé d'un programme est valide, alors "tout va bien" dans l'exécution du programme
• nous nous intéressons à la question de solvabilité d'un tel système d'équations (donc à une notion algorithmique, contrairement à la notion sémantique de validité).