CAV / SoftMC / GDV à Edimbourg : petit bilan personnel
Je suis revenu à Nantes le 14 juillet, enthousiaste sur ces neuf jours passés à Edimbourg.
D’un point de vue purement touristique, cette ville écossaise est résolument splendide et mérite les louanges qu’on en fait ici et là. La proximité de la nature est particulièrement appréciable : le siège d’Arthur en est un exemple frappant. En peu de temps (une heure de marche), on passe du centre-ville à un lieu duquel on domine toute la région. On a alors une vue à 360° des plus enchanteresses. `
Dans les pubs, le soir, l’ambiance est tranquille, reposante. Si on excepte l’accent - très marqué - des autochtones, les Ecossais me sont apparus comme des gens sympathiques et chaleureux. Bref, je reviens conquis.
La conférence CAV nous a réservé quelques surprises : par exemple, je ne m’attendais pas à ce que les systèmes temporisés soient si peu présents dans les exposés présentés pour l’occasion. Cette année, la majorité des résultats avancés concernait la vérification automatique de programmes informatiques, par des analyses discrètes. Problèmes de satisfiabilité SAT, solveurs associés, bounded model checking, .. étaient au coeur des préoccupations.
Si cette conférence n’a pas inspiré d’idées directement applicables à mon thème de recherche actuel, elle m’a toutefois permis d’élargir ma culture générale en terme de vérification (ce qui pourrait être utile pour de futures recherches).
Plus encore, ce que j’apprécie dans les conférences, ce sont toutes les rencontres qu’on y fait. On en apprend plus sur le fonctionnement dans d’autres laboratoires, sur les échanges que la communauté scientifique entretient, on découvre des parcours atypiques, on croise des références dans notre domaine de recherche, des chercheurs brillants - jeunes et moins jeunes. On mesure tout le chemin qui nous sépare de ces personnes et on a envie de marcher sur leurs traces. C’est tout à la fois une leçon d’humilité et une incitation à viser plus haut. L’émulation, il n’y a que ça de vrai.
Ce séjour à Edimbourg, c’était aussi pour moi l’occasion de mon premier exposé dans un workshop international. Si la présentation s’est passée sans problème majeur, je ne suis que moyennement satisfait de ma prestation. Je ne pense pas avoir enthousiasmé les foules. D’une part, parce que l’objet de notre étude dénotait un peu par rapport au reste de la conférence et du workshop. D’autre part, à cause de certaines maladresses de présentation dont je suis responsable. J’ai encore beaucoup de progrès à faire pour réussir des exposés en anglais clairs, attractifs et agréables à suivre. En tout cas, cette expérience aura été riche en enseignements. Cette mise en situation “réelle” me permet de mieux percevoir ce que je dois améliorer dans la structure de mon propos, dans mes transparents, dans la présentation générale.
J’ai du pain sur la planche.
Pour finir, quelques autres photos souvenirs de ce voyage.
- quelques vues depuis le siège d’Arthur et de la promenade que nous avons faite ;
- rien de tel qu’un plat indien pour se remplir l’estomac après s’être dépensé ;
- les petits déjeuners offraient un choix certain, placé notamment sous le signe du commerce équitable ;
- il est loin le temps du stress irraisonné avant les khôlles en prépa ; avant ma présentation, j’étais relativement serein ;
- dans les pubs, un certain nombre de jeux est mis à disposition ;
- les cheveux longs, ça permet de jouer avec le vent : avant / après ;
Sama It!
19/07/2005 à 00:25
En parlant de l’usage d’internet, je ne pense pas que l’outil soit la vrai problématique.
En d’autres termes, c’est l’utilisation de l’outil et les lois qui sanctionnent les abus qui doivent être mises au point.
Il est vrai que la fiabilité des systèmes va à l’encontre de leurs vulgarisation, mais nous avons vu apparaitre des sites ayant pignon sur rue ayant des pratiques douteuses pour ne pas dire plus. Or dans ce far west informatique, la loi du plus fort règne en maître, que ce soit les numéros de comptes bancaires qui se gardent après achat et qui sont parfois utilisés abusivement, aux noms de domaine détournés de force, aux promesses d’envoie non honorée sans remboursement, le travail sur internet ressemble plus à une rente pour quelques puissant (FAI, hébergeurs…). Je ne parle même pas des nombreuses tentatives de fraude de crève la faim, qui tente leur chance par tous les moyens.
Cordialement
19/07/2005 à 00:31
Disons pour être un peu plus précis que la conférence s’intéressait beaucoup à la vérification fonctionnelle au niveau implémentation (bug genre indice de tableau trop grand, pointeur nul voire mauvais résultats d’opérations arithmétiques) alors que ta thèse se place plutôt au niveau vérification de la correction temporelle de la spécification, soit bien plus en amont dans le cycle de production des logiciels.
Sinon, c’est vrai que c’était vraiment chouette (comme dirait Harry P.) cette petite semaine à Edimbourg :-)
19/07/2005 à 01:29
On peut mettre du html dans les petits commentaires ?
Bon, je teste, c’est plus simple… Et çacouleur ?
19/07/2005 à 01:31
Non, pour votre info, ça marche pas, la couleur…
Bon, j’arrête de faire n’importe quoi…
Bonne nuit.
19/07/2005 à 09:36
Temps > Je ne vois pas trop ce que ce commentaire vient faire là. Il faisait référence à un autre billet ?
Didier > Merci pour ces précisions, les lecteurs apprécieront :-)
Patricia > Oui, le HTML fonctionne dans les commentaires, mais pour un nombre restreint de balises seulement. Comme tu auras pu le constater, les balises de gras, italiques, [strong] emphasis sont acceptées :-)
19/07/2005 à 09:49
Je me dois d’apporter quelques corrections importantes à ton texte.
1) “le siège d’Arthur en est un exemple frappant. En peu de temps (une heure de marche)“: Je pense que par honnêteté, tu devrais remplacer le “une heure de marche” par “une heure de marche et quelques chutes“. :)
2) Concernant le sujet de la conférence, il s’agissait de vérification automatique de code. Et les problèmes SAT venaient essentiellement du fait que comme ces problèmes sont indécidables on utilise habituellement des techniques d’abstraction par prédicats (predicate abstraction) ou d’interprétation abstraite (abstract interpretation) qui requièrent de vérifier qu’une erreur dans le modèle abstrait peut s’exécuter dans le modèle concret. Et s’il ne peut pas, on doit extraire le plus petit nombre de prédicats à ajouter au modèle pour invalider la trace d’erreur qui n’est pas concrétisable afin de recommencer la vérification avec un modèle abstrait plus rafiné. Le théorème d’interpolation de Craig, permet d’obtenir ce nombre de prédicat mimum mais passe par la résolution d’un problème de satisfiabilité. D’où une recherche accrue dans des algorithmes efficaces (en temps et en précision) dans la génération de cette interpolation de Craig.
3) Le fait que les systèmes temporisés ne soient pas au centre des préoccupation c’est que ça marche pas ! :) Il reste encore à trouver des méthodes qui permettent de la génération automatique de code robuste. J.-F. Raskin (et, entre autre N. Markey) nous donnent bon espoir avec la sémantique AASAP. Mais tant que ce problème d’implémentation n’aura pas été réglé, des conférences comme CAV traiterons les systèmes temporisés comme tu l’a vu.
3) Elles sont toutes floues tes photos !!! 8-)
That’s all folks !
19/07/2005 à 09:53
Je retente juste une fois la couleur… ça serait vachement joli de mettre de la couleur partout.
Morgan, tu vas regretter de nous avoir filé l’adresse de ton site… :)
19/07/2005 à 09:53
Mince, j’ai raté. Tant pis.
19/07/2005 à 10:01
Mes lecteurs sont merveilleux !
Vous voyez, c’est cela qui fait toute la force des blogs : les lecteurs peuvent intervenir, corriger les erreurs ou zones de flou laissées par l’auteur, et participent ainsi au processus d’amélioration de l’ensemble. Il s’instaure un dialogue qui enrichit tant les lecteurs que l’auteur originel :-)
19/07/2005 à 11:06
C’est un amphi d’Appleton, ça (photo “avant ma présentation”) ? On dirait le lecture theatre A, B ou C derrière la DHT (David Hume Tower).
19/07/2005 à 11:20
Oui, oui, c’est bien un amphi d’Appleton. Je ne sais plus le numéro correspondant, mais c’est le grand amphi du premier étage d’Appleton ;-)
19/07/2005 à 17:35
OK, en HSS (Humanities Social Science) je n’ai jamais eu à y mettre les pieds (j’étais plutôt AFB, Adam Ferguson Building) dans les seminar rooms.
29/07/2005 à 00:57
[…] cier Emmanuel pour ses commentaires argumentés et instructifs (et aussi pour l’inviter à […]
08/09/2005 à 21:09
Very informed and interesting comments! Greetings.
online casinos