Un papier de plus…

Et oui, l’article suivant :

Uniform Monte-Carlo Model-Checking. Johan Oudinet, Alain Denise, Marie-Claude Gaudel, Richard Lassaigne and Sylvain Peyronnet.

a été accepté pour publication à FASE 2011 (le site web de la conférence est aussi accessible par là).

On y présente une méthode pour la génération uniforme de lassos dans les graphes de flots réductibles. Cela vous fait une belle jambe n’est ce pas ? En fait les lassos sont les structures qui permettent de déterminer la validité de certaines formules de la logique $latex LTL$ (Linear Temporal Logic). En les échantillonnant uniformément, on peut chercher des comportements spécifiques d’un système tout en maximisant la couverture de la méthode (c’est à dire sans privilégier certaines zones du système).

Pour ceux qui sont intéressés par les fondements des méthodes formelles de vérification de logiciels et autres systèmes, la liste des articles acceptés est disponible sur le site web : http://www.lsi.upc.edu/~orejas/Accepted.html, vous pourriez y trouver votre bonheur (ou pas).