Desole, je pensais etre un peu plus productif sur mon blog... Etant donne que je croule sous le boulot (je vous donne meme pas mes horraires j'en ai honte).
Ha oui tiens ! J'y pense je vous ai meme pas dit sur quoi je fais ma these. Alors si j'ai bien compris (ca commence bien) je travaille sur la verification formelle des noyaux de systemes d'exploitation. Kesako?? Bon un systeme d'exploitation que tout le monde connait: windows.
Le noyau c'est le programme qui tourne en boucle juste au dessus du materiel, qui le gere et qui offre des services a tout les autres programmes.
Mais pourquoi verifier ces machins vu que certains qui sont tout pourris (indice: ce systeme d'exploitation a deja ete nomme) remplissent (a peu pres) leur roles. Malheureux! Des OS (Sperating System, desole je suis super feneant) y'en a partout. Si votre PC plante c'est relativement pas grave (des fois si mais y'a tres peu souvent mort d'homme). Or des qu'il y a des processeurs/memoires/tout le tralala dans un dispositif, il y a forcement un OS. Et dans certain cas un crash resulte dans des pertes humaine/castastrophes. Des exemples ? Ba l'ABS de votre voiture, les instruments de vol des avions, les systemes des centrales nucleaire ...
Donc voila c'est la lourde tache qui m'incombe devant l'humanite (enfin devant ceux qui savent/comprennent ce que je fais, soit 3~4 personnes dans le monde).
Pour realiser cet exploit (qui reste a faire) j'utilise un theorem prover du nom de Coq (coq.inria.fr). Tres beau, tres pratique (comprendre aussi pratique que les ordinateurs des annees 50 et imbitable au possible, ca c'est un parfait exemple du double langage scientifique). D'ailleurs j'y retourne!!!
/https%3A%2F%2Fassets.over-blog.com%2Ft%2Fcedistic%2Fcamera.png)