Meetings

Kick-Off

Kick-Off Meeting of the CPP project.

Date

The Doodle has spoken, the Kick-Off Meeting will take place on November, 10th.

Please select your favorite date on the following doodle : http://www.doodle.com/3euxniby7grdsb5r

Place

The meeting will take place at CEA Saclay, in the "Siège" building. It is the blue spot on the map : http://maps.google.fr/maps/ms?ie=UTF8&msa=0&ll=48.72435,2.155026&spn=0.003503,0.008261&t=h&z=17

You can find indications on how to come to CEA on this page (in french) : http://www-centre-saclay.cea.fr/fr/fr/Acces-au-Centre-de-Saclay

To come to CEA "Siège", you can follow the "CEA Siège" signs from the "Christ de Saclay". There is also a bus, line 91.06, starting from Massy Palaiseau. You must get off at the "CEA - Porte 306" stop.

Program

The meeting will start at 10am and should end at 17pm. You can find a detailled program here: program-kick-off.pdf.

Talks :

  • Jean Goubault-Larrecq (LSV) : Incertitude, non-déterminisme et probabilités. Je vais tenter de résumer certains aspects principaux du pavé (voir http://www.lsv.ens-cachan.fr/~goubault/). L'aspect principal de ces travaux est qu'ils fondent une approche générale de modélisation de systèmes de transition sur des espaces infinis impliquant trois formes de "flou" que l'on ne confond que trop souvent: - le choix non déterministe, où intuitivement un scheduler (angélique, démoniaque ou erratique) vient vous dire quelle action entreprendre; - le choix probabiliste, où l'on tire au hasard l'action à entreprendre; - l'incertitude, où les actions à entreprendre et les états dans lesquelles nous sommes ne sont même pas complètement déterminés. Les deux premiers points peuvent servir a priori à modéliser les comportements des arrondis ou des erreurs de mesure dans le cadre de CPP, alors que le troisième est ce dont on a besoin pour faire des analyses statiques, fondées sur la notion d'approximation. Techniquement, le troisième point s'obtient grâce à une approche dite de théorie des domaines (et plus généralement, via des topologies non séparées). Le mélange des deux autres points mène à deux modèles, celui des capacités (à la Choquet), et celui des prévisions (à la Walley). Je ne pourrai pas parler de tout, mais j'essaierai d'arriver à parler : - de l'aspect effectif des choses; pas au sens d'algorithmes, mais au sens de théorèmes assurant l'existence d'approximants par exemple à toute prévision continue, par des prévisions dites simples, lesquelles semblent devoir généraliser la notion de P-box;- de (pseudo-)distances et d'hémi-distances de (bi)simulation, ce qui doit être relié au WP4.

Attach:jgl-kickoff-cpp.pdf

  • Dale Miller (INRIA Saclay) : An overview of model checking work in Parsifal. Over the past few years, we have been developing means to view model checking as deduction. The connections we have found between these two topics has had several benefits. (1) We can view standard model-checking problems as theorem proving (proof search) within simple logics of fixed points. (2) Given the connection to deduction, we could generalize model checking from working over simple domains (eg, vectors of values over finite domains) to more complex domains that involve syntax (even syntax with bindings). (3) Backtracking search, unification, and tabled deduction can all be applied to the implementation of model checking. (4) Connections to linear logic and to game semantics lie just below the surface of the model-checking-as-deduction approach. I will give an overview of these topics and discuss the prototype systems Bedwyr that the team has built. Connections to probabilistic model checking will be next to consider.

Attach:miller-10-11-09.pdf

  • Olivier Bouissou (CEA LIST) : Hybrid extensions of numerical programs: semantics and analysis. In this talk, I will present some recent progress we made on the static analysis of numerical control-command programs. Such programs are in constant interaction with a physical environment through sensors and actuators. Their behaviour is thus tightly linked with the behaviour of the (continuous time) environement that they control. However, this interaction is most often not taken into account when it comes to the verification of such programs: abstract interpretation based analyzer usually abstract the values given by the sensors by an interval and forget about the actuators. If this gives correct results, this also limits the precision of the analysis. In this talk, I will explain how we can in fact integrate the physical environement in the static analysis of control command programs and how this leads to new kinds of proofs. After a brief review of the static analysis techniques for numerical programs used in Fluctuat, I will focuss my talk on two subjects: 1. how we can give a (concrete) semantics for models made of a (discrete) program in interaction with a (continuous) environment. 2. how we can abstract this semantics, and in particular how we can abstract the continuous evolution.

Attach:bouissou-cpp-kick-off.pdf

  • Michel Kieffer (Supélec L2S) : Estimation paramètrique à erreurs bornées de systèmes décrits par des modèles dynamiques continus en utilisant des fonctions de sensibilité.

Attach:D: Δ\L2S_Kick_Off_CEA_11_09.pdf

  • Philippe Chaput (ENS Cachan) : Approximating Markov Processes by Averaging

Par manque de temps, présentation reportée à une réunion ultérieure.

  • Eric Goubault (CEA LIST) : Some very basic thoughts on CPP and analysis of numerical computations. Dans cet expose peu prepare, je donnerai quelques exemples qui, je l'espere, motiveront quelques developpements dans le cadre du projet CPP.

Attach:slidesCPP-2.pdf

(you need to download the following .mov files for the videos attached to slidesCPP-2.pdf; you need Adobe acrobat reader version >=9.0 and the quicktime plugin to view this correctly)

Attach:Householder3.mov

Attach:HouseholderMontage01_huit.mov

Attach:Filterset-DIGITEOnew.mov

Participants

  • Olivier Bouissou (CEA LIST)
  • Jean Goubault-Larrecq (ENS Cachan)
  • Catuscia Palamidessi (INRIA Saclay)
  • Dale Miller (INRIA Saclay)
  • Sylvie Putot (CEA LIST)
  • Eric Goubault (CEA LIST, après-midi uniquement)
  • Philippe Chaput (ENS Cachan)
  • Emmanuel Ledinot (Dassault-Aviation)
  • Erick Herbin (Dassault-Aviation, après-midi uniquement)
  • Stéphane Gaubert (INRIA Saclay)
  • Paul Poncet (INRIA Saclay)
  • Michel Kieffer (Supélec LSS)
  • Daniel Poulton (Supélec SSE)
  • Ivan Gazeau (INRIA Saclay)
  • Philippe Baufreton (Hispano-Suiza)