Le projet Isaac et Benoit Sonntag recherche assez urgement un thésard pour septembre 2007.
Une bourse est proposée avec cette thèse.
Le texte est très vague (normal pour une thèse), mais j'en préciserai les possibilités concrètes plus bas.
Proposition de thèse (Sept. 2007) pour étudiant ayant un Master 2
d'informatique dans lequel il est particulièrement bien classé.
Directeur(s) de Thèse : Philippe Clauss, PR - Benoît Sonntag, MCF
Unité(s) d'Accueil(s) : Laboratoire LSIIT UMR CNRS 7005, Strasbourg,
équipe ICPS
Établissement de rattachement : Université Louis Pasteur, Strasbourg
Requis :
- Interêt pour le projet Isaac/Lisaac (http://isaacos.loria.fr/),
- Très bonne connaissance des concepts objets,
- Bonne connaissance des systèmes d'exploitation,
- Connaissance en Architecture et Assembleur.
Contacts :
sonntag __at __ icps.u-strasbg.fr ou
clauss__at __icps.u-strasbg.fr
Titre : Programmation des couches basses par une approche de haut niveau
Sujet (résumé) :
L'informatique embarquée impose une réutilisabilité croissante du code
existant avec de fortes contraintes matérielles. Néanmoins dans la
pratique, l'équipe de développement doit maîtriser en profondeur ce code
pour l'adapter aux différentes contraintes matérielles. Le code est
essentiellement écrit en C pour des raisons d'efficacité, de portage,
d'intégration avec le système (gestion du matériel). Ici, nous dénonçons
une réutilisabilité peu fiable, parfois hasardeuse d'un code C non
maîtrisé.
Les langages de haut niveau échappent encore à la programmation système.
Le développement des couches basses nécessite un code sensible à
l'architecture matérielle et rend difficile l'application
d'optimisations génériques et automatiques. La fiabilisation des couches
basses du système devient une priorité grandissante dans une
informatique de plus en plus hétéroclite. Une impasse est alors à
combattre: la réutilisabilité et la fiabilisation d'un code sont
grandement facilitées par l'utilisation des langages de haut niveau,
mais leurs utilisations pour les couches basses du système ne sera
possible qu'après une maîtrise des optimisations spécifiques du matériel
avec des performances au moins similaires à un programme écrit en C.
Cette thèse aura pour objectif de sortir de cette impasse en repoussant
les limites des langages de haut niveau pour l'embarqué tout en
garantissant l'efficacité.
Une des possibilités de recherche pour le futur thésard serait un projet passionnant et ambitieux : Certains savent peut être que Lisaac est un langage à contrat, comme Eiffel.
Il existe à l'heure actuelle peu de compilateur permettant de produire du code certifié, et lorsque cela existe, les performances ne sont que rarement au rendez vous.
Il s'agirait donc ici de produire un prouveur de code, qui prendrai les contrats définis dans le code et vérifierai si ces contrats sont respectés par le code écris.L'utilisation de logiciels de preuve comme coq peut être envisagée (1)
C'est une hypothèse parmi d'autres...
Les avantages du projet, permettant de disposer d'un cadre accueillant sont :
-La maîtrise du compilateur :
Lisaac est un compilateur écris par Benoit Sonntag, (dont la prochaine version totalement réécrite va être bientôt publiée), à ce titre le langage est totalement maîtrisé par l'encadrant de thèse, et les modifications nécessaires lors de cette thèse pourront être faites directement dans le compilateur.
- Lisaac est un langage minimaliste construit autour d'environ 10 primitives, en ce sens, il est moins difficile à prouver.
- Analyse de flot. Lisaac est le premier compilateur objet à intègrer de l'analyse de flot, c'est à dire une analyse de toutes les possibilités d'exécutions du code.
- Performances. Lisaac est un compilateur capable d'optimiser son code de sorte à ce qu'il soit aussi rapide (ou presque) qu'un même algorithme écrit en C.
- Lisaac est écrit en Lisaac.
N'hésitez pas à en parler autour de vous.
(1) why de Jean-Christophe Filliâtre est un logiciel qui explore une problématique similaire, dans une sorte de caml, mais il subsiste quelques trous. http://why.lri.fr/index.fr.html
Journal Le projet Isaac cherche un thésard (bourse de thèse)
2
avr.
2007
# Financement?
Posté par Duncan Idaho . Évalué à 4.
J'imagine que vous ne proposez pas une thèse bénévole, et comme l'argent ne pousse pas sur les arbres...
[^] # Re: Financement?
Posté par ナイコ (site web personnel) . Évalué à 10.
[^] # Re: Financement?
Posté par Matthieu Moy (site web personnel) . Évalué à 7.
[^] # Re: Financement?
Posté par Julien CARTIGNY (site web personnel) . Évalué à 2.
Par contre, il serait bien de préciser un peu la bourse en question...
[^] # Re: Financement?
Posté par Ontologia (site web personnel) . Évalué à 3.
- Soit c'est une MENRT (bourse du ministère) -> 1400 ¤ net /mois
- Soit une bourse régionale/CNRS , compter jusqu'à 1700 ¤ net /mois
Je ne peux pas en dire plus pour le moment.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Financement?
Posté par zerbro . Évalué à 2.
Et ma copine, qui a une bourse MENRT ne touche pas du tout 1400 ¤ net/mois.
A moins que tu inclues le monitorat avec les bourses ? Mais meme dans ce cas, je ne crois pas qu'on atteigne les sommes données.
Les montants sont donc a vérifier (ou alors on se fait sacrément avoir, et j'aimerais savoir ou aller réclamer mon manque à gagner !)
[^] # Re: Financement?
Posté par Ontologia (site web personnel) . Évalué à 1.
Je pense que le monitorat est compris dans ce salaire.
Tu peux aussi lui poser la question :-)
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Financement?
Posté par zerbro . Évalué à 2.
Les reponses sont ici :
http://www.sg.cnrs.fr/drh/emploi-nonperm/bdi.htm#cnrs
Donc 1700¤ brut, c'est CNRS/entreprise
Sinon, c'est 1400¤ brut (CNRS, CNRS/region, CNRS/Region/Entreprise).
A moins que ca ne soit pas une bourse BDI, mais un autre type de bourse ?
Je n'ai pas vérifié pour les bourses ministérielles, mais je pense qu'il faut remplacer "net" par "brut".
[^] # Re: Financement?
Posté par Dr BG . Évalué à 2.
# Loi toubon
Posté par Yann 'Ze' Richard (site web personnel) . Évalué à 5.
http://www.culture.gouv.fr/culture/dglf/lois/loi-fr.htm
Je voit en signataire le ministre de l'enseignement supérieur et de la recherche tutelle des organismes de recherches, donc j'imagine qu'ils sont concernés ?
[^] # Re: Loi toubon
Posté par Ontologia (site web personnel) . Évalué à 2.
sonntag __at __ icps.u-strasbg.fr
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Loi toubon
Posté par Ontologia (site web personnel) . Évalué à 2.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Loi toubon
Posté par melalcoolique . Évalué à 6.
[^] # Re: Loi toubon
Posté par Thomas Douillard . Évalué à 2.
1) tous ceux qui ont le niveau pour lire les documents en questions sont bilingues
2) le nombre de personnes qui liront est très faible.
Pour une thèse par exemple, une pratique assez courante est de reprendre des articles déja écris pour rédiger la version finale de la thèse. Or la plupart de ces articles sont écris ... en anglais. Quand on sait ce qu'est la phase de rédaction d'une thèse, on comprends facilement que ce soit un calvaire de faire de la traduction à ce moment.
Faire la traduction, c'est du boulot, ça prends du temps, et du temps en général, on en manque, alors ça peut facilement passer à la trappe ...
[^] # Re: Loi toubon
Posté par chl (site web personnel) . Évalué à 2.
In this article we will see ...
# prouveur ?
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
Le truc qui pourra manipuler le dénombrement des ensembles comme dans cduce pour vérifier des choses comme l'empreinte mémoire maximum et pour permètre des optimisations de code ?
"La première sécurité est la liberté"
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.