Postdoctoral position at LIX, Ecole Polytechnique
Forum 'Emplois' - Sujet créé le 2008-02-14 par Leo Liberti
LIX, Ecole Polytechnique --- Postdoc announcement
Optimization of fixed-point formats in numerical programs
Leo Liberti
LIX, Ecole Polytechnique, 91128 Palaiseau, France
leoliberti@gmail.com
A post-doctoral fellowship of 1 year is open at LIX (Laboratoire
d'Informatique), the computer science department of Ecole
Polytechnique in Palaiseau, near Paris (France), linked with a
national project called EDONA, subsidised by the french ministry of
industry.
Research topic. Embedded systems, such as engine controllers,
fly-by-wire or X-by-wire computers, airbag controllers to mention but
a few, rely on numerical algorithms. However, the embedded
implementation can only use finite precision arithmetic (as opposed to
floating point), and hence exhibits imprecision errors with respect to
the true real number computation. In general, these numerical
algorithms are tested according to floating point specifications,
hence their reliability in finite precision arithmetic is not clearly
ascertained. The overall goal of this project is to optimize the size
(number of digits before and after the comma) of fixed point
(i.e. finite precision) variables involved in the numerical algorithm,
with the objective to be no less precise than the floating point
computation, with respect to the real number computation. The
technique that we put forward in this project is the static analysis
of the code by abstract interpretation , that is, the automatic
determination of computer program properties, by over-approximations,
from the source code and without any executions. We have already
applied it to the determination of good bounds for the floating point,
fixed point (in a given format) and real values of program variables,
together with good bounds for the imprecision error, which is
implemented in the tool FLUCTUAT. The aim of this postdoc is to
develop a method and tool for optimizing the number of bits required
to make a given calculation in fixed point format, according to
several objectives; one of which is, as specified above, that of being
no less precise than the floating point computation (our current line
of work includes modelling a similar problem by means of a
mathematical programming formulation). Ultimately, we want to develop
a black-box/grey-box optimizer, linked with the floating-point
semantics and a very simple fixed-point semantics implemented in
FLUCTUAT. Further information can be found at the following web page:
http://www.di.ens.fr/~goubault/ (static analysis)
General information. This postdoc is funded partially by Ecole
Polytechnique and partially by the EDONA project (a sub-project of the
Ile-de-France competitivity pole ``System@tic''). The candidate will
work within the MeASI (Mode'lisation et Analyse de Syste`mes en
Interaction) research group, and in particular with Leo Liberti,
Daniel Krob, Sylvie Putot and Eric Goubault. The successful candidate
should be familiar mainly with static analysis of code, model
checking, semantics and verification, and secondarily with modelling,
optimization and algorithmics. Required technical skills: C/C++,
verification codes, and optionally AMPL/CPLEX. Since we know that it
is extremely unlikely to find the perfect match to all these
requirements, candidates with subsets of the listed skills are
encouraged to apply --- but must be prepared to invest some time in
acquiring the missing knowledge if retained. Candidates with some
industrial experience are also encouraged to apply. The postdoctoral
position, physically located at LIX, Ecole Polytechnique, is paid
around 2000e/month after social charges but before income tax (so the
net amount should be between 1700 and 1800 euros / month, which is
enough to live decently in Paris without a family to provide for). The
contract can be started as early as possible after mutual
agreement. The position will be available until filled, but to ensure
a full consideration, please submit the following application material
by 28 February 2008, in either English (preferred) or French.
Application procedure. Applications must be made in electronic
form. Zip all your PDF files specified below (that's ZIP, not RAR or
any other compressed format) into a single file called surname.zip and
send it to leoliberti@gmail.com.
A full CV: education, positions filled, research interests,
involvement in funded projects, teaching experience, academic visits
and seminars, programming and technical skills, spoken/written
languages, publication list (refereed journals, refereed conference
papers, theses, other published material, technical reports,
patents, software documentation). Name this file
surname-cv.pdf.
A covering letter specifying why you think you would be a good
match for the position. If you are missing some of the required
skills / knowledge, but you still think you would be a good
candidate, you can explain why here, and what you plan to do to
acquire the missing skills. Name this file
surname-covering.pdf.
A copy of the most relevant papers you have published (papers
``accepted for publication'' count as published, submitted papers
count as technical reports). Name this file
surname-paper-.pdf, where ranges over the
size of your paper production.
A copy of your Ph.D. thesis, and if appropriate also of your
M.Sc. thesis. Name these files surname-phd.pdf and
surname-msc.pdf.
WARNING: All material must be submitted in PDF format. Other
formats (including MS Office) will not be considered.
Optimization of fixed-point formats in numerical programs
Leo Liberti
LIX, Ecole Polytechnique, 91128 Palaiseau, France
leoliberti@gmail.com
A post-doctoral fellowship of 1 year is open at LIX (Laboratoire
d'Informatique), the computer science department of Ecole
Polytechnique in Palaiseau, near Paris (France), linked with a
national project called EDONA, subsidised by the french ministry of
industry.
Research topic. Embedded systems, such as engine controllers,
fly-by-wire or X-by-wire computers, airbag controllers to mention but
a few, rely on numerical algorithms. However, the embedded
implementation can only use finite precision arithmetic (as opposed to
floating point), and hence exhibits imprecision errors with respect to
the true real number computation. In general, these numerical
algorithms are tested according to floating point specifications,
hence their reliability in finite precision arithmetic is not clearly
ascertained. The overall goal of this project is to optimize the size
(number of digits before and after the comma) of fixed point
(i.e. finite precision) variables involved in the numerical algorithm,
with the objective to be no less precise than the floating point
computation, with respect to the real number computation. The
technique that we put forward in this project is the static analysis
of the code by abstract interpretation , that is, the automatic
determination of computer program properties, by over-approximations,
from the source code and without any executions. We have already
applied it to the determination of good bounds for the floating point,
fixed point (in a given format) and real values of program variables,
together with good bounds for the imprecision error, which is
implemented in the tool FLUCTUAT. The aim of this postdoc is to
develop a method and tool for optimizing the number of bits required
to make a given calculation in fixed point format, according to
several objectives; one of which is, as specified above, that of being
no less precise than the floating point computation (our current line
of work includes modelling a similar problem by means of a
mathematical programming formulation). Ultimately, we want to develop
a black-box/grey-box optimizer, linked with the floating-point
semantics and a very simple fixed-point semantics implemented in
FLUCTUAT. Further information can be found at the following web page:
http://www.di.ens.fr/~goubault/ (static analysis)
General information. This postdoc is funded partially by Ecole
Polytechnique and partially by the EDONA project (a sub-project of the
Ile-de-France competitivity pole ``System@tic''). The candidate will
work within the MeASI (Mode'lisation et Analyse de Syste`mes en
Interaction) research group, and in particular with Leo Liberti,
Daniel Krob, Sylvie Putot and Eric Goubault. The successful candidate
should be familiar mainly with static analysis of code, model
checking, semantics and verification, and secondarily with modelling,
optimization and algorithmics. Required technical skills: C/C++,
verification codes, and optionally AMPL/CPLEX. Since we know that it
is extremely unlikely to find the perfect match to all these
requirements, candidates with subsets of the listed skills are
encouraged to apply --- but must be prepared to invest some time in
acquiring the missing knowledge if retained. Candidates with some
industrial experience are also encouraged to apply. The postdoctoral
position, physically located at LIX, Ecole Polytechnique, is paid
around 2000e/month after social charges but before income tax (so the
net amount should be between 1700 and 1800 euros / month, which is
enough to live decently in Paris without a family to provide for). The
contract can be started as early as possible after mutual
agreement. The position will be available until filled, but to ensure
a full consideration, please submit the following application material
by 28 February 2008, in either English (preferred) or French.
Application procedure. Applications must be made in electronic
form. Zip all your PDF files specified below (that's ZIP, not RAR or
any other compressed format) into a single file called surname.zip and
send it to leoliberti@gmail.com.
A full CV: education, positions filled, research interests,
involvement in funded projects, teaching experience, academic visits
and seminars, programming and technical skills, spoken/written
languages, publication list (refereed journals, refereed conference
papers, theses, other published material, technical reports,
patents, software documentation). Name this file
surname-cv.pdf.
A covering letter specifying why you think you would be a good
match for the position. If you are missing some of the required
skills / knowledge, but you still think you would be a good
candidate, you can explain why here, and what you plan to do to
acquire the missing skills. Name this file
surname-covering.pdf.
A copy of the most relevant papers you have published (papers
``accepted for publication'' count as published, submitted papers
count as technical reports). Name this file
surname-paper-.pdf, where ranges over the
size of your paper production.
A copy of your Ph.D. thesis, and if appropriate also of your
M.Sc. thesis. Name these files surname-phd.pdf and
surname-msc.pdf.
WARNING: All material must be submitted in PDF format. Other
formats (including MS Office) will not be considered.