@InProceedings{ baarir.04.mascots, author = {Souheib Baarir and Jean-Michel Ili{\'e} and Alexandre Duret-Lutz}, title = {Improving Reachability Analysis for Partially Symmetric High Level Petri Nets}, booktitle = {Proceedings of the Poster Session of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04)}, editors = {Pete Harrison and Doug DeGroot}, year = {2004}, address = {Volendam, The Netherlands}, month = oct, pages = {5--8}, pdf = {adl/baarir.04.mascots.pdf}, poster = {adl/baarir.04.mascots.poster.pdf} } @TechReport{ baarir.06.tr03, author = {Souheib Baarir and Alexandre Duret-Lutz}, title = {Emptiness Check of Powerset {B\"u}chi Automata}, institution = {Universit{\'e} Pierre et Marie Curie, LIP6-CNRS}, year = {2006}, type = {Technical report}, number = {2006/003}, address = {Paris, France}, month = oct, pdf = {adl/baarir.06.tr03.pdf}, abstract = {A possible attack on the state explosion of the automata-theoretic approach to model-checking is to build an automaton B whose states represent sets of states of the original automaton A to check for emptiness. This paper introduces two emptiness checks for B{\"u}chi automata whose states represent sets that may include each other. The first check on B is equivalent to a traditional emptiness check on A but uses inclusion tests to direct and further reduce the on-the-fly construction of B. The second check is impressively faster but may return false negatives. We illustrate and benchmark both using a symmetry-based reduction.} } @InProceedings{ baarir.07.acsd, author = {Souheib Baarir and Alexandre Duret-Lutz}, title = {Emptiness Check of Powerset {B\"u}chi Automata}, booktitle = {Proceedings of the 7th International Conference on Application of Concurrency to System Design (ACSD'07)}, editors = {Twan Basten and Gabriel Juh{\'a}s and Sandeep Shukla}, year = {2007}, month = jul, pages = {41--50}, publisher = {IEEE Computer Society}, pdf = {adl/baarir.07.acsd.pdf}, slides = {adl/baarir.07.acsd.slides.pdf}, abstract = {We introduce two emptiness checks for B{\"u}chi automata whose states represent sets that may include each other. The first is equivalent to a traditional emptiness check but uses inclusion tests to direct the on-the-fly construction of the automaton. The second is impressively faster but may return false negatives. We illustrate and benchmark the improvement on a symmetry-based reduction.} } @InProceedings{ baarir.07.msr, author = {Souheib Baarir and Alexandre Duret-Lutz}, title = {Test de vacuit{\'e} pour automates de {B\"u}chi ensemblistes avec tests d'inclusion}, booktitle = {Actes du 6e Colloque Francophone sur la Mod{\'e}lisation des Syst{\`e}mes R{\'e}actifs (MSR'07)}, editors = {Jean-Michel Muller and {\'E}ric Niel and Laurent Pi{\'e}trac}, publisher = {Hermes-Lavoisier}, year = {2007}, month = oct, pages = {19--34}, abstract = {Nous pr{\'e}sentons deux algorithmes d'emptiness check pour les automates de B{\"u}chi dont les {\'e}tats sont des ensembles qui peuvent s'inclure les uns les autres. Le premier est {\'e}quivalent {\`a} un emptiness check traditionnel, mais utilise des tests d'inclusion pour diriger la construction {\`a} la vol{\'e}e de l'automate. Le second est beaucoup plus rapide, mais peut retourner de faux n{\'e}gatifs. Nous illustrons et {\'e}valuons l'am{\'e}lioration avec une r{\'e}duction bas{\'e}e sur les sym{\'e}tries.} } @InProceedings{ burrus.03.mpool, author = {Nicolas Burrus and Alexandre Duret-Lutz and Thierry G\'eraud and David Lesage and Rapha\"el Poss}, title = {A Static {C++} Object-Oriented Programming (SCOOP) Paradigm Mixing Benefits of Traditional OOP and Generic Programming}, booktitle = {Proceedings of the Workshop on Multiple Paradigm with OO Languages (MPOOL'03)}, year = {2003}, address = {Anaheim, California}, month = oct, pdf = {adl/burrus.03.mpool.pdf}, proceedings = {http://www.fz-juelich.de/nic-series/volume27/volume27.html} , abstract = {Object-oriented and generic programming are both supported in C++. OOP provides high expressiveness whereas GP leads to more efficient programs by avoiding dynamic typing. This paper presents SCOOP, a new paradigm which enables both classical OO design and high performance in C++ by mixing OOP and GP. We show how classical and advanced OO features such as virtual methods, multiple inheritance, argument covariance, virtual types and multimethods can be implemented in a fully statically typed model, hence without run-time overhead.} } @TechReport{ clouard.99.tr, author = {R\'egis Clouard and Abderrahim Elmoataz and Fran\c{c}ois Angot and Olivier Lezoray and Alexandre Duret-Lutz}, title = {Une biblioth\`eque et un environnement de programmation d'op\'erateurs de traitement d'images}, institution = {GREYC-ISMRA}, year = {1999}, number = {99008}, address = {Caen, France}, month = nov, url = {http://www.greyc.ismra.fr/~regis/Pandore/} } @InProceedings{ couvreur.05.spin, author = {Jean-Michel Couvreur and Alexandre Duret-Lutz and Denis Poitrenaud}, title = {On-the-Fly Emptiness Checks for Generalized {B\"u}chi Automata}, booktitle = {Proceedings of the 12th International SPIN Workshop on Model Checking of Software}, pages = {143--158}, year = {2005}, editor = {Patrice Godefroid}, volume = {3639}, series = {Lecture Notes in Computer Science}, month = aug, publisher = {Springer-Verlag}, pdf = {adl/couvreur.05.spin.draft.pdf}, slides = {adl/couvreur.05.spin.slides.pdf}, abstract = { Emptiness check is a key operation in the automata-theoretic approach to LTL verification. However, it is usually done on B{\"u}chi automata with a single u acceptance condition. We review existing on-the-fly emptiness-check algorithms for generalized B{\"u}chi automata (i.e., with multiple acceptance conditions) and u show how they compete favorably with emptiness-checks for degeneralized automata, especially in presence of weak fairness assumptions. We also introduce a new emptiness-check algorithm, some heuristics to improve existing checks, and propose algorithms to compute accepting runs in the case of multiple acceptance conditions. } } @InProceedings{ darbon.02.ismm, author = {J\'er\^ome Darbon and Thierry G\'eraud and Alexandre Duret-Lutz}, title = {Generic Implementation of Morphological Image Operators}, booktitle = {Mathematical Morphology, Proceedings of the 6th International Symposium (ISMM)}, pages = {175--184}, year = {2002}, address = {Sydney, Australia}, month = apr, publisher = {Sciro Publishing}, pdf = {adl/darbon.02.ismm.pdf}, abstract = { Several libraries dedicated to mathematical morphology exist. But they lack genericity, that is to say, the ability for operators to accept input of different natures---2D binary images, graphs enclosing floating values, etc. We describe solutions which are integrated in Olena, a library providing morphological operators. We demonstrate with some examples that translating mathematical formulas and algorithms into source code is made easy and safe with Olena. Moreover, experimental results show that no extra costs at run-time are induced. } } @InProceedings{ demaille.08.fsmnlp, author = {Akim Demaille and Alexandre Duret-Lutz and Florian Lesaint and Sylvain Lombardy and Jacques Sakarovitch and Florent Terrones}, title = {An {XML} format proposal for the description of weighted automata, transducers, and regular expressions}, booktitle = {Proceedings of the seventh international workshop on Finite-State Methods and Natural Language Processing (FSMNLP'08)}, year = {2008}, address = {Ispra, Italia}, month = sep, abstract = {We present an XML format that allows to describe a large class of finite weighted automata and transducers. Our design choices stem from our policy of making the implementation as simple as possible. This format has been tested for the communication between the modules of our automata manipulation platform Vaucanson, but this document is less an experiment report than a position paper intended to open the discussion among the community of automata software writers.}, pdf = {adl/demaille.08.fsmnlp.pdf} } @InProceedings{ duret.00.gcseyrw, author = {Alexandre Duret-Lutz}, title = {Olena: a Component-Based Platform for Image Processing, mixing Generic, Generative and {OO} Programming}, booktitle = {Proceedings of 2nd International Symposium on Generative and Component-Based Software Engineering (GCSE 2000)}, publisher = {Young Researchers Workshop (published in ``Net.ObjectDays2000'')}, year = {2000}, address = {Erfurt, Germany}, pages = "653--659", month = oct, url = {http://www.lrde.epita.fr/dload/papers/gcse00-yrw/olena.html} } @TechReport{ duret.00.tr01, author = {Alexandre Duret-Lutz and Thierry G{\'e}raud}, title = {Improving Object-Oriented Generic Programming}, institution = {EPITA Research and Development Laboratory}, year = {2000}, type = {Technical Report}, number = {0001}, address = {Paris}, month = apr, pdf = {adl/duret.00.tr01.pdf}, abstract = { Great efforts have gone into building scientific libraries dedicated to particular application domains and a main issue is to manage the large number of data types involved in a given domain. An ideal algorithm mplementation should be general: it should be written once and process data in an abstract way. Moreover, it should be efficient. For several years, some libraries have been using generic programming to address this problem. In this report, we present two major improvements of this paradigm. \par In generic libraries, a concept is the description of a set of requirements on a type that parameterizes an algorithm implementation (the notion of concept replaces the classical object-oriented notion of abstract class). A problem is that, until now, concepts are only defined in the documentation. We managed to make them explicit in the program by representing a concept by a type; moreover, (multiple) concept inheritance is fully supported. The procedure signature thus evolves from \texttt{void foo(AbstractA\&)} for classic object-orientation, and from \texttt{template void foo(A\&)} for classic generic programming, towards \texttt{template void foo(ConceptA\&)}. This results in a better support of procedure overloading, which is of prime importance for libraries where each algorithm implementation can have numerous variations. \par Another problem is that the generic programming paradigm suffers from a lack of appropriate design patterns. We observed that classical patterns of Gamma et al. can be translated into this paradigm while handling operation polymorphism by parametric polymorphism. In these patterns, method calls can be solved statically, because the inferior type of each object in generic programming is known at compile-time. We thus preserve their modularity and reusability properties but we avoid the performance penalty due to their dynamic behavior, which is a critical issue in numerical computing. This results in better design capabilities for object-oriented generic libraries. } } @InProceedings{ duret.01.ae, author = {Alexandre Duret-Lutz}, title = {Expression Templates in {Ada}}, booktitle = {Proceedings of the 6th International Conference on Reliable Software Technologies (Ada-Europe'01)}, year = {2001}, address = {Leuven, Belgium}, month = may, pages = {191--202}, volume = {2043}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, note = {Best paper award.}, pdf = {adl/duret.01.ae.pdf}, abstract = {High-order matrix or vector expressions tend to be penalized by the use of huge temporary variables. Expression templates is a C++ technique which can be used to avoid these temporaries, in a way that is transparent to the user. We present an Ada adaptation of this technique which---while not transparent---addresses the same efficiency issue as the original. We make intensive use of the signature idiom to combine packages together, and discuss its importance in generic programming. Finally, we express some concerns about generic programming in Ada.} } @InProceedings{ duret.01.coots, author = {Alexandre Duret-Lutz and Thierry G\'eraud and Akim Demaille}, title = {Design Patterns for Generic Programming in {C++}}, booktitle = {Proceedings of the 6th USENIX Conference on Object-Oriented Technologies and Systems (COOTS'01)}, year = {2001}, address = {San Antonio, Texas, USA}, month = jan, pages = {189--202}, publisher = {USENIX Association}, pdf = {adl/duret.01.coots.pdf}, url = {http://www.usenix.org/publications/library/proceedings/coots01/duret.html} , abstract = {Generic programming is a paradigm whose wide adoption by the C++ community is quite recent. In this scheme most classes and procedures are parameterized, leading to the construction of general and efficient software components. In this paper, we show how some design patterns from Gamma et al. can be adapted to this paradigm. Although these patterns rely highly on dynamic binding, we show that, by intensive use of parametric polymorphism, the method calls in these patterns can be resolved at compile-time. In intensive computations, the generic patterns bring a significant speed-up compared to their classical peers. } } @MastersThesis{ duret.03.msc, author = {Alexandre Duret-Lutz and Rachid Rebiha}, title = {SPOT\,: une biblioth{\`e}que de v{\'e}rification de propri{\'e}t{\'e}s de logique temporelle {\`a} temps lin{\'e}aire}, school = {DEA Syst{\`e}mes Informatiques R{\'e}partis, Universit{\'e} de Paris 6}, month = sep, year = {2003}, pdf = {adl/duret.03.msc.pdf} } @InProceedings{ duret.04.mascots, author = {Alexandre Duret-Lutz and Denis Poitrenaud}, title = {SPOT: an Extensible Model Checking Library using Transition-based Generalized {B\"u}chi Automata}, booktitle = {Proceedings of the 12th IEEE/ACM International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS'04)}, editors = {Doug DeGroot and Pete Harrison}, year = {2004}, address = {Volendam, The Netherlands}, month = oct, publisher = {IEEE Computer Society}, pages = {76--83}, pdf = {adl/duret.04.mascots.draft.pdf}, abstract = { Spot is a C++ library offering model checking bricks that can be combined and interfaced with third party tools to build a model checker. It relies on Transition-based Generalized B{\"u}chi Automata (TGBA) and does not need to degeneralize these automata to check their emptiness. We motivate the choice of TGBA by illustrating a very simple (yet efficient) translation of LTL into TGBA. We then show how it supports on-the-fly computations, and how it can be extended or integrated in other tools. } } @PhDThesis{ duret.07.phd, author = {Alexandre Duret-Lutz}, title = {Contributions {\`a} l'approche automate pour la v{\'e}rification de propri{\'e}t{\'e}s de syst{\`e}mes concurrents}, school = {Universit{\'e} Pierre et Marie Curie (Paris 6)}, year = {2007}, month = jul, pdf = {adl/duret.07.phd.pdf}, slides = {adl/duret.07.phd.slides.pdf}, www = {../th.html} } @InProceedings{ duret.09.atva, author = {Alexandre Duret-Lutz and Denis Poitrenaud and Jean-Michel Couvreur}, title = {On-the-fly Emptiness Check of Transition-based {S}treett Automata}, booktitle = {Proceedings of the 7th International Symposium on Automated Technology for Verification and Analysis (ATVA'09)}, year = {2009}, editor = {Zhiming Liu and Anders P. Ravn}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, pages = {213--227}, volume = {5799}, pdf = {adl/duret.09.atva.pdf}, slides = {adl/duret.09.atva.slides.pdf}, abstract = {In the automata theoretic approach to model checking, checking a state-space $S$ against a linear-time property $\varphi$ can be done in $\RO(|S|\times 2^{\RO(|\varphi|)})$ time. When model checking under $n$ strong fairness hypotheses expressed as a Generalized B{\"u}chi automaton, this complexity becomes $\RO(|S|\times 2^{\RO(|\varphi|+n)})$.\par Here we describe an algorithm to check the emptiness of Streett automata, which allows model checking under $n$ strong fairness hypotheses in $\RO(|S|\times 2^{\RO(|\varphi|)}\times n)$. We focus on transition-based Streett automata, because it allows us to express strong fairness hypotheses by injecting Streett acceptance conditions into the state-space without any blowup.} } @TechReport{ duret.99.tr03, author = {Alexandre Duret-Lutz and Thierry G\'eraud}, title = {Patrons de conception statiques pour la programmation g\'en\'erique en {C++}}, institution = {EPITA Research and Development Laboratory}, year = {1999}, type = {Technical Report}, number = {9903}, address = {Paris}, month = sep, pdf = {adl/duret.99.tr03.pdf} } @InProceedings{ geraud.00.europlop, author = {Thierry G\'eraud and Alexandre Duret-Lutz}, title = {Generic Programming Redesign of Patterns}, booktitle = {Proceedings of the 5th European Conference on Pattern Languages of Programs (EuroPLoP'00)}, year = {2000}, month = jul, page = {283--294}, editor = {M. Devos and A. R\"uping}, publisher = {UVK, Univ. Verlag, Konstanz}, adress = {Irsee, Germany}, pdf = {adl/geraud.00.europlop.pdf} } @InProceedings{ geraud.00.icpr, author = {Thierry G\'eraud and Yoann Fabre and Alexandre Duret-Lutz and Dimitri Papadopoulos-Orfanos and Jean-Fran\c{c}ois Mangin}, title = {Obtaining Genericity for Image Processing and Pattern Recognition Algorithms}, booktitle = {Proceedings of the 15th International Conference on Pattern Recognition (ICPR'00)}, year = {2000}, month = sep, address = {Barcelona, Spain}, volume = {4}, pages = {816--819}, publisher = {IEEE Computer Society}, abstract = { Algorithm libraries dedicated to image processing and pattern recognition are not reusable; to run an algorithm on particular data, one usually has either to rewrite the algorithm or to manually "copy, paste, and modify". This is due to the lack of genericity of the programming paradigm used to implement the libraries. In this paper, we present a recent paradigm that allows algorithms to be written once and for all and to accept input of various types. Moreover, this total reusability can be obtained with a very comprehensive writing and without significant cost at execution, compared to a dedicated algorithm. This new paradigm is called "generic programming" and is fully supported by the C++ language. We show how this paradigm can be applied to image processing and pattern recognition routines. The perspective of our work is the creation of a generic library.} } @InProceedings{ geraud.01.ai, author = {Thierry G\'eraud and Yoann Fabre and Alexandre Duret-Lutz}, title = {Applying Generic Programming to Image Processing}, booktitle = {Proceedings of the IASTED International Conference on Applied Informatics (AI'01)---Symposium Advances in Computer Applications}, year = {2001}, address = {Innsbruck, Austria}, month = feb, pages = {577--581}, publisher = {ACTA Press}, editor = {M.H.~Hamsa}, abstract = { This paper presents the evolution of algorithms implementation in image processing libraries and discusses the limits of these implementations in terms of reusability. In particular, we show that in C++, an algorithm can have a general implementation; said differently, an implementation can be generic, i.e., independent of both the input aggregate type and the type of the data contained in the input aggregate. A total reusability of algorithms can therefore be obtained; moreover, a generic implementation is more natural and does not introduce a meaningful additional cost in execution time as compared to an implementation dedicated to a particular input type. } } @TechReport{ geraud.99.tr01, author = {Thierry G\'eraud and Alexandre Duret-Lutz}, title = {Composants g\'en\'eriques de calcul scientifique}, institution = {EPITA Research and Development Laboratory}, year = {1999}, type = {Technical Report}, number = {9901}, address = {Paris}, month = mar, pdf = {adl/geraud.99.tr01.pdf}, abstract = {Dans le cadre de l'{\'e}criture en C++ d'une biblioth{\`e}que de traitements d'images et d'un atelier de programmation par composants d'une cha{\^i}ne de traitements, nous nous sommes fix{\'e}s deux objectifs principaux : rendre les traitements g{\'e}n{\'e}riques vis-{\`a}-vis du type de ses entr{\'e}es sans entra{\^i}ner de surco{\^u}t significatif {\`a} l'ex{\'e}cution, et pouvoir ex{\'e}cuter un traitement lorsqu'il a et{\'e} introduit ult{\'e}rieurement {\`a} la compilation de l'atelier. \par Le premier objectif est atteint a l'aide de programmation g{\'e}n{\'e}rique et de la traduction en polymorphisme statique de certains idiomes (\textit{design patterns}) d{\'e}finis pour le polymorphisme dynamique. La probl{\'e}matique du second objectif est double. Tout d'abord, nous devions r{\'e}aliser la mise en correspondance d'un traitement dont les entr{\'e}es-sorties sont des types abstraits et de la routine g{\'e}n{\'e}rique, charg{\'e}e du traitement, dont les param{\`e}tres sont des types concrets ; ensuite, nous devions pouvoir compiler et lier de nouveaux traitements a la vol{\'e}e, lors de l'ex{\'e}cution de l'atelier. Pour atteindre ce double objectif, nous utilisons de la programmation g{\'e}n{\'e}rative et nous pratiquons l'instanciation paresseuse (\textit{lazy}) de code g{\'e}n{\'e}rique.\par Les solutions que nous apportons permettent la gestion de composants r{\'e}utilisables de calcul scientifique, ce qui, {\`a} notre connaissance, est original. } } @Article{ thierry-mieg.04.gl, author = {Yann Thierry-Mieg and Souheib Baarir and Alexandre Duret-Lutz and Fabrice Kordon}, title = {Nouvelles techniques de model-checking pour la v{\'e}rification de syst{\`e}mes complexes}, journal = {G{\'e}nie Logiciel}, year = {2004}, number = {69}, pages = {17--23}, month = jun, pdf = {adl/thierry-mieg.04.gl.pdf} } @InProceedings{ xue.03.icip, author = {Heru Xue and Thierry G{\'e}raud and Alexandre Duret-Lutz}, title = {Multi-band Segmentation using Morphological Clustering and Fusion; Application to Color Image Segmentation}, booktitle = {Proceedings of the IEEE International Conference on Image Processing (ICIP 2003)}, year = {2003}, address = {Barcelona, Spain}, month = sep, abstract = { In this paper we propose a novel approach for color image segmentation. Our approach is based on segmentation of subsets of bands using mathematical morphology followed by the fusion of the resulting segmentation "channels". For color images the band subsets are chosen as RG, RB and GB pairs, whose 2D histograms are processed as projections of a 3D histogram. The segmentations in 2D color spaces are obtained using the watershed algorithm. These 2D segmentations are then combined to obtain a final result using a region split-and-merge process. The CIE $L^*a^*b^*$ color space is used to measure the color distance. Our approach results in improved performance and can be generalized for multiband segmentation of images such as multi-spectral satellite images. } }