[TYPES/announce] PostDoc position on certifying Network Calculus computations within Isabelle

[Marc Boyer]

A PostDoc position is open for 12 month at ONERA (Toulouse,
France), to work on an encoding of Network Calculus within the
interactive proof assistant Isabelle.

Network Calculus is a formal theory designed to compute delays and
buffer usage in networks. It has been used to certify the A380
backbone. Its mathematical background is based on the (min,plus) dioid,
and algorithms have been derived and implemented that allow users to
ascertain bounds on network parameters, given hypotheses on the
arrival of packets from the environment. The objective of the
post-doctoral research will be to contribute to increasing the
confidence in the results obtained by applying Network Calculus.
The candidate is expected to encode the mathematical theory
of Network Calculus in the theorem prover Isabelle/HOL and to derive
theorems underlying the algorithms for network analysis. The results
will be validated by instrumenting a Network Calculus analyzer in order
to produce a trace whose correctness can be certified using Isabelle.

Preliminary work has already been carried out in order to demonstrate
the feasibility of the approach, and the post-doctoral researcher will
extend and consolidate the existing Isabelle theory. The work will be
carried out at ONERA, in partnership with SME Real-Time at Work, and 
INRIA Nancy (Stephan Merz).

Please do not hesitate to contact Marc Boyer (Marc.Boyer at onera.fr) with
any questions if you are interested in the position.
-- 
Marc Boyer, Ingenieur de recherche                              ONERA
Tel: (33)  5.62.25.26.36                                         DTIM
Fax: (33)  5.62.25.26.93                          2, av Edouard Belin
http://www.onera.fr/staff/marc-boyer/          31055 TOULOUSE Cedex 4