Plusieurs annonces dans la lettre cette semaine : le classement du comité de sélection aux postes de Maîtres de Conférence 109 et 110 de l’Université de Paris à l’IRIF, les résultats du concours CNRS INS2I/Section 6 (Informatique fondamentale) et 8 postes d’ATER en informatique mis à concours à l’UFR d’Informatique.
Côté actualités scientifiques, à lire l’article de B.Guinard et A. Korman récemment publié dans Science Advances et un zoom sur l’article qui a remporté le Concur Test of Time Award 2021.
A ne pas manquez, la date de clôture de l’appel à projets Emergence (29 avril 11h00, heure de Paris) : n’hésitez pas à réutiliser des demandes existantes, même celles qui auraient été rejetées au 1er tour de l’ANR.
Pour les intéressés, le Service Culturel de l’Université de Paris lance 2 projets culturels. Si ces initiatives vous intéressent, manifestez-vous auprès de cadet@irif.fr.
Et enfin, un rappel important concernant les procédures d’achat réclamant un financement : toujours contacter le secrétariat, en particulier pour les demandes de remboursement.
Bonne lecture !
Initialement présenté lors de la conférence Concur 1997, l’article « Reachability Analysis of Pushdown Automata : Application to Model-checking » co-écrit par Ahmed Bouajjani (IRIF), Javier Esparza (Technische Universität München) et Oded Maler reçoit, 24 ans plus tard, le Concur Test of Time Award 2021.
Le prix récompense les réalisations importantes en matière de théorie de la concurrence publiées lors d’une conférence Concur et ayant résisté avec succès à l’épreuve du temps. Cet article constitue une percée dans le domaine de la vérification formelle. Il présente une méthode devenue un standard en matière de vérification des systèmes infinis. L'article porte sur la vérification de systèmes modélisés par des automates à pile, un modèle fondamental avec de multiples applications, notamment en vérification de programmes procéduraux. L'idée principale est d'utiliser les automates d'états-finis pour la représentation et la manipulation d'ensembles potentiellement infinis de configurations lors de l'analyse d'un tel modèle.
L'article considère la classe générale des automates à pile alternants et présente une procédure simple, basée sur les automates finis, pour l'analyse d'accessibilité et le calcul des configurations accessibles. La procédure est ensuite utilisée pour résoudre plusieurs problèmes de model-checking (vérification qu'un modèles satisfait une propriété exprimée dans différentes logiques temporelles pour la spécification de comportements). Cet article a eu un impact important sur la communauté, concernant aussi bien les fondements (algorithmes de model-checking, jeux, etc.) que les applications (techniques et outils de vérification de programmes récursifs, concurrents, etc.)