BACK TO INDEX

Publications of year 2004

Books and proceedings

  1. M. Huisman and T. Jensen, editors. J. Logic and Algebraic Programming. Special issue on Formal Methods for Smart Cards, vol. 58(1-2), 2004. Elsevier. 
    @Proceedings{Huisman:04:JLAPSmartCards,
editor = "M. Huisman and T. Jensen",
title = "J.~Logic and Algebraic Programming. Special issue on Formal Methods for Smart Cards, vol.~58(1-2)",
publisher = "Elsevier",
year = "2004",

}


Thesis

  1. B. Morin. Corrélation d'alertes issues d'outils de détection d'intrusions avec prise en compte d'informations sur le système surveillé. PhD thesis, INSA de Rennes, Février 2004. 
    @PhDThesis{Morin04,
Author={B. Morin},
Title={Corrélation d'alertes issues d'outils de détection d'intrusions avec prise en compte d'informations sur le système surveillé},
School={INSA de Rennes},
Year={2004},
Month={Février} 
}


  2. Katell Morin-Allory. Vérification formelle dans le modèle polyédrique. PhD thesis, Université de Rennes 1, Octobre 2004. 
    @PhDThesis{alloy-morin04,
Author={Katell Morin-Allory},
Title={Vérification formelle dans le modèle polyédrique},
School={Université de Rennes 1},
Year={2004},
Month={Octobre}
}


Articles in journal or book chapters

  1. M. Eluard and T. Jensen. Vérification du contrôle d'accès dans des cartes à puce multi-application. Technique et Science Informatiques, 23(3):323-358, 2004. 
    @Article{Eluard:04:TSI,
author = {M. Eluard and T. Jensen},
title = {Vérification du contrôle d'accès dans des cartes à puce multi-application},
Journal = {Technique et Science Informatiques},
volume = "23",
number = "3",
pages = "323--358",
year = "2004" 
}


  2. G. Feuillade, T. Genet, and V. Viet Triem Tong. Reachability Analysis over Term Rewriting Systems. Journal of Automated Reasoning, 33 (3-4):341-383, 2004. [WWW] Keyword(s): Term Rewriting, Reachability, Tree Automata, Approximations, Verification, Timbuk, Abstract Interpretation.
    This paper surveys some techniques and tools for achieving reachability analysis over term rewriting systems. The core of those techniques is a generic tree automata completion algorithm used to compute in an exact or approximated way the set of descendants (or reachable terms). This algorithm has been implemented in the Timbuk tool. Furthermore, we show that many classes with regular sets of descendants of the literature corresponds to specific instances of the tree automata completion algorithm and can thus be efficiently computed by Timbuk. An extension of the completion algorithm to conditional term rewriting systems and some applications are also presented.

    @ARTICLE{FeuilladeGVTT-JAR04,
AUTHOR = "Feuillade, G. and Genet, T. and Viet Triem Tong, V.",
TITLE = "{R}eachability {A}nalysis over {T}erm {R}ewriting {S}ystems",
JOURNAL= jar,
YEAR = {2004},
VOLUME = {33 (3-4)},
PAGES = {341-383},
URL = {http://www.irisa.fr/lande/genet/publications.html},
KEYWORDS = {Term Rewriting, Reachability, Tree Automata, Approximations, Verification, Timbuk, Abstract Interpretation},
ABSTRACT= {This paper surveys some techniques and tools for achieving reachability analysis over term rewriting systems. The core of those techniques is a generic tree automata completion algorithm used to compute in an exact or approximated way the set of descendants (or reachable terms). This algorithm has been implemented in the Timbuk tool. Furthermore, we show that many classes with regular sets of descendants of the literature corresponds to specific instances of the tree automata completion algorithm and can thus be efficiently computed by Timbuk. An extension of the completion algorithm to conditional term rewriting systems and some applications are also presented.},

}


  3. T. Jensen and J.-L. Lanet. Modélisation et vérification dans les cartes à puce. Revue d'électricité et de l'électronique, 6/7:89-94, 2004. 
    @Article{Jensen:04:CartesAPuce,
author = "T. Jensen and J.-L. Lanet",
title = "Modélisation et vérification dans les cartes à puce",
journal = "Revue d'électricité et de l'électronique",
year = "2004",
volume = "6/7",
pages = "89--94" 
}


Conference articles

  1. David Cachera, Thomas Jensen, David Pichardie, and Vlad Rusu. Extracting a data flow analyser in constructive logic. In Proc. ESOP'04, number 2986 of Springer LNCS, pages 385 - 400, 2004. 
    @InProceedings{CachJen:esop04,
author = {David Cachera and Thomas Jensen and David Pichardie and Vlad Rusu},
title = {Extracting a data flow analyser in constructive logic},
booktitle = "Proc.~ESOP'04",
series = "Springer LNCS",
number = "2986",
pages = "385 -- 400",
year = "2004" 
}


  2. Matthieu Petit and Arnaud Gotlieb. An ongoing work on statistical structural testing via probabilistic concurrent constraint programming. In Proc. of SIVOES-MODEVA workshop, St Malo, France, November 2004. IEEE.
    The use of a model to describe and test the expected behavior of a program is a well-proved software testing technique. Statistical structural testing aims at building a model from which an input probability distribution can be derived that maximizes the coverage of some structural criteria by a random test data generator. Our approach consists in converting statistical structural testing into a Probabilistic Concurrent Constraint Programming (PCCP) problem in order 1) to exploit the high declarativity of the probabilistic choice operators of this paradigm and 2) to benefit from its automated constraint solving capacity. This paper reports on an ongoing work to implement PCCP and exploit it to solve instances of statistical structural testing problems. Application to testing Java Card applets is discussed.

    @InProceedings{PG04,
author = "Matthieu Petit and Arnaud Gotlieb",
title = "An ongoing work on statistical structural testing via probabilistic concurrent constraint programming",
pages = "",
booktitle = "Proc. of SIVOES-MODEVA workshop",
year = "2004",
publisher = "IEEE",
address = "St Malo, France",
month = "November",
abstract = {The use of a model to describe and test the expected behavior of a program is a well-proved software testing technique. Statistical structural testing aims at building a model from which an input probability distribution can be derived that maximizes the coverage of some structural criteria by a random test data generator. Our approach consists in converting statistical structural testing into a Probabilistic Concurrent Constraint Programming (PCCP) problem in order 1) to exploit the high declarativity of the probabilistic choice operators of this paradigm and 2) to benefit from its automated constraint solving capacity. This paper reports on an ongoing work to implement PCCP and exploit it to solve instances of statistical structural testing problems. Application to testing Java Card applets is discussed.} 
}


  3. Matthieu Petit and Arnaud Gotlieb. Probabilistic choice operators as global constraints : application to statistical software testing. In Poster presentation in ICLP'04, number 3132 of Springer LNCS, pages 471 - 472, 2004. 
    @InProceedings{PetitGotlieb:04:poster,
author = {Matthieu Petit and Arnaud Gotlieb},
title = {Probabilistic choice operators as global constraints : application to statistical software testing},
booktitle = "Poster presentation in ICLP'04",
series = "Springer LNCS",
number = "3132",
pages = "471 -- 472",
year = "2004" 
}



BACK TO INDEX

This document was translated from BibTEX by bibtex2html