Postdoctoral position at ENS Cachan - LSV and CEA LIST - MeASI
--------------------------------------------------------------------------
Credibilistic and Prevision-Theoretic Semantics and
Analysis of Numerical Programs
Contact:
------------
Jean Goubault-Larrecq goubault@lsv.ens-cachan.fr
Eric Goubault eric.goubault@cea.fr
Olivier Bouissou olivier.bouissou@cea.fr
Project description:
---------------------------
This postdoctoral position is part of the ANR Blanc ``Confidence, Proof
and Probabilities'' project:
http://www.lix.polytechnique.fr/~bouissou/cpp/
This project aims at studying the joint use of probabilistic and
deterministic semantics and analysis methods in order to improve the
applicability and precision of static analysis methods on numerical
programs. The project includes theoretical computer scientists,
specialists of abstract interpretation based static analysis, applied
mathematicians and control theoreticians as well as industrial partners.
The project will contain the following steps:
* construction of good approximations of the semantics for
non-deterministic and probabilistic behaviours.
* abstraction of these semantics models for the tractable static
analysis of complex programs and test case generation.
* characterisation of the imprecision error due to the use of floating
point numbers by the program.
The role of this postdoctoral position is to explore the theoretical and
practical aspects of these points. A first task will be to define a good
semantics for probabilistic behaviours in numerical programms, building
on work by Goubault-Larrecq at LSV [ICALP07,PRONOBIS], in particular the
notion of prevision transition systems [FOSSACS08]. Then, the candidate
will explore the abstraction semantics, based on deterministic
abstractions using zonotopes as in [CAV09,arxiv2008,arxiv2010]. Finally,
if time permits and according to the applicants preferences, he/she may
look into the notion of bisimulation distances to characterize the
imprecision error.
Qualifications:
----------------
The candidate must have a PhD in computer science or applied mathematics
and be specialist of one of the following subject: probabiliy theory,
static analysis, numerical programs analysis,...
Practical information:
----------------------
This work will be done in very close collaboration with co-advisors from
two sites (Jean Goubault-Larrecq at LSV and Eric Goubault at CEA LIST),
and will be deeply associated with the project.
The candidate will be located both at ENS Cachan, and at CEA Saclay
nearby Paris. Salaries range from 27840 to 30000 euros per year.
References:
-----------
[CAV2009] Khalil Ghorbal, Eric Goubault, Sylvie Putot, "The Zonotope
Abstract Domain Taylor1+", CAV 2009.
[Arxiv2010] Eric Goubault, Sylvie Putot, "A zonotopic framework for
functional
abstractions", CoRR abs/0910.1763.
[Arxiv2008] Eric Goubault, Sylvie Putot, "Perturbed affine arithmetic
for invariant computation in numerical program analysis", CoRR
abs/0807.2961
[ICALP07] Jean Goubault-Larrecq, "Continuous Capacities on Continuous
State Spaces", ICALP 07, LNCS 4596.
[FOSSACS08] Jean Goubault-Larrecq, "Prevision Domains and Convex
Powercones", FOSSACS 2008, LNCS 4962.
[PRONOBIS] Jean Goubault-Larrecq, "Une introduction aux capacites, aux
jeux et aux previsions", available at
http://www.lsv.ens-cachan.fr/~goubault/ProBobis/pp.pdf.
Olivier Bouissou
--
Ingenieur Chercheur - CEA List
Tel : +33 1 69 08 88 59
Fax: +33 1 69 08 83 95
Mel : olivier.bouissou@cea.fr
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************
Posts
