Réunion Geccoo

Nancy
LORIA-Salle B013

27/28 Juin 2005

1  Participants

2  Programme

Lundi 27 Juin

13h00

DÉJEÛNER

14h00

Accueil

14h15

Frédéric Dadeau
Titre : Perspectives sur la génération de test à partir de JML
Résumé : La génération de test actuelle à partir de JML s'articule autour de la production massive et semi-automatique de tests unitaires destinés à être exécutés avec JMLUnit (l'outil d'exécution de test unitaires pour Java, combinant le RunTime Assertion Checker de JML et JUnit). A l'opposé, la méthode de génération de tests dits "aux limites" --comme celle de BZ-Testing-Tools (BZ-TT)-- consiste à produire, à partir d'un modèle formel (par ex. en B), des cas de tests pour la validation d'une implantation. Pour ce faire, une séquence d'exécution est automatiquement calculée à partir du modèle, en fonction d'une stratégie bien particulière. Celle-ci vise à placer le système dans un état précis pour chercher à activer un comportement spécifique décrit dans le modèle. Cet exposé s'attachera à présenter l'originalité et la pertinence de l'application d'une telle approche à la génération de test à partir de JML. Nous aborderons les perspectives d'applications de ces techniques à la génération de tests à partir de JML. Enfin, nous discuterons des différentes stratégies de génération de tests qui peuvent être mises en place pour la détection de problèmes/bugs potentiels inhérents aux programmes orientés-objets (héritage, polymorphisme, liaisons dynamiques, etc).

15h00

Nicolas Ayache
Titre : Collaboration d'outils de preuve interactifs et automatiques
Résumé : Cet exposé présente les résultats d'un stage de Master M2 effectué dans l'équipe Démons au LRI. Ce stage s'inscrit dans le contexte de la vérification formelle de programmes à l'aide des outils développés dans cette équipe (Why, Krakatoa, Caduceus). Dans la situation actuelle, cette activité de preuve formelle peut être conduite soit à l'aide d'outils de preuve interactive (Coq, PVS, etc.), soit à l'aide d'outils de preuve automatique (Simplify, haRVey, CVC, etc.) mais ces outils ne communiquent pas entre eux. En particulier, lorsqu'une obligation n'est pas prouvée automatiquement l'utilisateur se retrouve condamné à une preuve interactive, donc laborieuse. Pour y remédier, nous proposons une intégration d'outils de preuve automatique externes, tels que ceux mentionnés ci-dessous, dans l'assistant de preuve Coq. Une architecture générique a été mise en place pour cette collaboration, consistant tout d'abord à traduire la logique de Coq vers la logique du premier ordre avec égalité et arithmétique entière, et ensuite à traduire cette logique du premier ordre vers les outils de preuve existants. La traduction vers la logique du premier ordre est ainsi factorisée. Nous décrirons le fragment de la logique de Coq supporté par cette traduction, et nous illustrerons notre exposé par de nombreux exemples.

15h30

Duc K. Tran
Title: On Superposition-Based Satisfiability Procedures and their Combination
Abstract: We study how to efficiently combine satisfiability procedures built by using a superposition calculus with satisfiability procedures for arbitrary theories, for which the superposition calculus may not apply (e.g., for various decidable fragments of Arithmetic). Our starting point is the Nelson-Oppen combination method, where satisfiability procedures cooperate by exchanging entailed (disjunction of) equalities between variables. We show that the superposition calculus deduces sufficiently many such equalities for convex theories (e.g., the theory of equality and the theory of lists) and disjunction of equalities for non-convex theories (e.g., the theory of arrays) to guarantee the completeness of the combination method. We also show how to make satisfiability procedures built by superposition both incremental and resettable by reusing the standard Congruence Closure algorithm.

16h00

PAUSE

20h00

Diner (Excelsior?)

Mardi 28 Juin

09h00

Sylvain Boulmé
Titre: Raffinement d'ordre supérieur, terminaison, et typage de l'espace des états.
Résumé: Dans cet exposé, je montrerai comment représenter l'espace des états en raffinement d'ordre supérieur. A partir de cette représentation, on peut imaginer plusieurs sémantiques pour l'espace des états. Une première sémantique, la plus générale, consiste à donner une sémantique de "tas" à l'espace des états ("tas" qui devient donc une sorte d'état global). Dans cette sémantique, il est toutefois difficile de donner des conditions simples pour:

• la préservation d'invariants.
• la terminaison des programmes en présence d'ordre sup.

Considérons par exemple le programme ML ci-dessous qui boucle :
let f = ref (fun () -> ())
in (f := fun () -> (!f) ()) ;
(!f) ()
Par ailleurs, le travail de spécification du programmeur est lui-aussi plus compliqué.
Je propose donc d'étudier une sémantique plus restreinte (sémantique de "pile", sans alias) qui permet d'aborder ces problèmes de façon plus simple.

09h45

Julien Roussel
Titre : Intégration de Krakatoa et des outils JML
Résumé : Afin de donner à Krakatoa un support complet du langage JML, nous proposons une nouvelle architecture qui intègre à Krakatoa les outils d'analyse syntaxique, de typage et de désucrage de JML. Ces derniers étant écrits en Java, la communication avec Krakatoa (écrit en Objective Caml) s'est faite par l'intermédiaire de fichiers XML. À cette fin, une DTD respectant JML a été conçue, afin d'assurer la validité des données partagées. Une seconde partie du travail a été une étude de cas : une preuve d'algorithmes sur des listes chainées, considérés comme représentatifs des difficultés rencontrées dans la preuve de programmes avec pointeurs.

10h30

PAUSE

11h00

DISCUSSION-PLAN DE TRAVAIL

12h45

DÉJEUNER

13h30

FIN DE LA RÉUNION