Search by property
This page provides a simple browsing interface for finding entities described by a property and a named value. Other available search interfaces include the page property search, and the ask query builder.
List of results
- Seminar/2012-02-15 + («The effective exploitation of his powers … «The effective exploitation of his powers of abstraction must be</br>regarded as one of the most vital activities of a competent</br>programmer.» disait Dijsktra.</br></br>En effet, pour aborder la complexité d'un problème, l'explicitation</br>des concepts utiles à sa formalisation et à sa résolution est bien</br>souvent une étape clé. Lorsque que l'on étend ce processus à une</br>classe de problèmes qui partagent les mêmes concepts, il est naturel</br>de se doter d'un langage le plus approprié possible pour manipuler ces</br>abstractions spécifiques à un domaine (en anglais, «Domain Specific</br>Language»).</br></br>Comment implémenter ces DSLs? Une première approche classique reflète</br>les constructions du DSL sous la forme d'un jeu de fonctions de</br>bibliothèque. L'avantage de cette approche est d'utiliser directement</br>son langage généraliste préféré, et sa chaîne de compilation</br>optimisée, de façon à générer du code machine à moindre frais. Par</br>contre, dans ce cadre, l'écriture de passe d'optimisations spécifiques</br>au DSL - à moins d'utiliser des techniques pointues de</br>méta-programmation - est a priori impossible.</br></br>Une seconde approche, opposée, consiste à écrire un compilateur pour</br>le DSL à partir de zéro. Toute liberté est alors donnée à</br>l'implémenteur d'intégrer à son compilateur des passes d'optimisation</br>spécifiques… mais au prix d'une réimplémentation de passes de</br>compilation déjà présentes, et certainement plus abouties, dans le</br>compilateur de son langage généraliste favori.</br></br>Dans cet exposé, je présenterai les travaux de Martin Odersky et</br>son équipe sur la virtualisation de DSLs à l'intérieur du langage de</br>programmation Scala. La virtualisation de langage utilise</br>intensivement le polymorphisme et la composition mixin de Scala ainsi</br>que des techniques de génération de code à l'exécution pour embarquer</br>des langages spécifiques dans Scala dont la compilation peut</br>réutiliser des modules du compilateur mais aussi étendre ces derniers</br>par des optimisations spécifiques au domaine. des optimisations spécifiques au domaine.)
- Seminar/2011-02-09 + (Nous étudions la problématique du mélange … Nous étudions la problématique du mélange de paradigmes de programmation</br>variés plongés dans un environnement concurrent. Dans cette</br>perspective, nous poursuivons</br>un cheminement similaire à celui qui conduit du lambda-calcul aux</br>langages fonctionnels, mais</br>en prenant comme point de départ le π-calcul. Nous proposons la</br>machine abstraite des π-threads</br>dont la principale originalité est l’absence de pile d’exécution.</br>Cette caractéristique</br>permet de nous reposer dans nos implémentations sur des algorithmes</br>simples et naturellement</br>concurrents, notamment pour ce qui concerne l’ordonnancement et le</br>ramasse-miettes. Pour ce</br>dernier, nous proposons un algorithme permettant de récupérer très</br>simplement les cycles de</br>processus en interblocage et autres structures bloquantes.erblocage et autres structures bloquantes.)
- Seminar/2021-10-06 + (Optimal transport (OT) has recently gained … Optimal transport (OT) has recently gained a lot of interest in machine learning. It is a natural tool to compare in a geometrically faithful way probability distributions. It finds applications in both supervised learning (using geometric loss functions) and unsupervised learning (to perform generative model fitting). OT is however plagued by the curse of dimensionality, since it might require a number of samples which grows exponentially with the dimension. In this talk, I will review entropic regularization methods which define geometric loss functions approximating OT with a better sample complexity.mating OT with a better sample complexity.)
- Seminar/2011-05-18 + (Pour encoder de manière efficace une séque … Pour encoder de manière efficace une séquence vidéo, la redondance</br>temporelle est souvent utilisée. Pour cela, le mouvement entre l'image</br>considérée et une image de référence est estimé. Cela permet de</br>générer une prédiction à partir de l'image de référence et seule la</br>différence entre la prédiction et l'image réelle est enregistrée. Pour</br>estimer ce mouvement, les codecs se contentent souvent de suivre</br>l'évolution spatiale de blocs dans l'image. Ils associent, pour chaque</br>bloc de l'image considérée, un bloc similaire dans un voisinage proche</br>dans l'image de référence. Nous présentons ici une méthode originale</br>pour réaliser cette prédiction par compensation de mouvement. Notre</br>méthode utilise les distances tangentes. Cela permet non seulement</br>d'estimer l'évolution de la position des blocs de l'image mais en</br>partie aussi l'évolution du bloc lui-même. Nos prédictions sont donc</br>de meilleure qualité. Utilisée dans l'encodage de séquences, on peut</br>espérer un gain de compression non négligeable. Pour valider</br>l'efficacité de la méthode, nous intégrons cette méthode dans le codec</br>Theora et mesurons son efficacité en comparant les résultats obtenus</br>avec notre méthode et ceux obtenus par une stratégie classique (le</br>block-matching).e stratégie classique (le block-matching).)
- Seminar/2009-02-11 + (JoCaml est une extension d'Objective Caml … JoCaml est une extension d'Objective Caml pour la programmation</br>concurrente et distribuée, inspirée par le join-calcul. Nous avons</br>récemment publié une nouvelle version de JoCaml, dont la compatibilité</br>avec OCaml est meilleure que celle de la version initiale de F. Le</br>Fessant. La nouvelle version pourra facilement être mise à jour au</br>rythme d'OCaml et est binaire-compatible avec OCaml.</br></br>L'exposé s'attachera plus au langage JoCaml qu'au système JoCaml. Il</br>montrera comment, à partir d'un programme potentiellement</br>parallélisable écrit en OCaml (le ray tracer du concours ICFP 2001),</br>on peut facilement produire un programme distribué, dans le cas</br>abordé, très efficace. Ce sera l'occasion d'aborder la programmation</br>en JoCaml de la coordination de multiples agents coopérants, d'une</br>manière simple et concise dans l'esprit de la programmation</br>fonctionnelle.</br></br>JoCaml est disponible en http://jocaml.inria.fr/.est disponible en http://jocaml.inria.fr/.)
- Seminar/2018-12-14 + (Recent advances in medical image computing … Recent advances in medical image computing have resulted in automated systems that closely assist physicians in patient</br>therapy. Computational and personalized patient models benefit diagnosis, prognosis and treatment planning, with a</br>decreased risk for the patient, as well as potentially lower cost. HeartFlow Inc. is a successful example of a company</br>providing such a service in the cardiovascular context. Based on patient-specific vascular model extracted from X-ray CT</br>images, they identify functionally significant disease in large coronary arteries. Their combined anatomical and</br>functional analysis is nonetheless limited by the image resolution. At the downstream scale, a functional exam called</br>Myocardium Perfusion Imaging (MPI) highlights myocardium regions with blood flow deficit. However, MPI does not</br>functionally relate perfusion to the upstream coronary disease. The goal of our project is to build the functional</br>bridge between coronary and myocardium. To this aim we propose an anatomical and functional extrapolation. We produce an</br>innovative vascular network generation method extending the coronary model down to the microvasculature. In the</br>resulting vascular model, we compute a functional analysis pipeline to simulate flow from large coronaries to the</br>myocardium, and to enable comparison with MPI ground-truth data.ble comparison with MPI ground-truth data.)
- Seminar/2019-03-06 + (Rendre la vue à ceux qui l’ont perdue a lo … Rendre la vue à ceux qui l’ont perdue a longtemps été considéré comme un sujet réservé à la science-fiction. Cependant,</br>sur les vingt dernières années les efforts intensifiés dans le domaine des prothèses visuelles ont abouti à des avancées</br>significatives, et plusieurs centaines de patients dans le monde ont reçu de tels dispositifs. Ce séminaire présentera</br>brièvement le domaine des prothèses rétiniennes avec une focalisation particulière sur les aspects de traitement</br>d’image. Nous exposerons les principales approches, les limitations connues et les résultats. les limitations connues et les résultats.)
- Seminar/2013-03-27 + (SMIL est une bibliothèque de traitement d' … SMIL est une bibliothèque de traitement d'images 2D/3D. Elle a été</br>développée pour répondre à une demande de plus en plus forte (en</br>particulier dans le cas de projets industriels) en termes de</br>performances : taille d'images (2D ou 3D) et temps d'exécution.</br>Développée en C++ et utilisant les templates, elle peut être utilisée</br>avec n'importe quel type standard de données. Un effort important a</br>été porté sur la factorisation du code (par le biais de functors),</br>d'une part, pour faciliter l'intégration de nouvelles fonctions, et</br>d'autre part pour concentrer les parties du code permettant</br>l'optimisation. Ces "briques" communes optimisées utilisent le code</br>SIMD généré par l'auto-vectorisation de gcc et sont également</br>parallélisées grâce à l'utilisation d'OpenMP.allélisées grâce à l'utilisation d'OpenMP.)
- Seminar/2008-03-26 + (Separation of concerns is the idea of brea … Separation of concerns is the idea of breaking down a program into</br>encapsulated pieces that overlap in functionality as little as</br>possible. Encapsulated entities, such as classes, methods or modules,</br>are more manageable, easier to test and maintain, and may be reused</br>more easily than a large, entangled program. A cross-cutting concern</br>is something that cannot be encapsulated using normal abstraction</br>mechanisms, thus defeating separation of concerns. A classical example</br>of this is logging (e.g., logging calls and returns to a file while</br>the program is running) - the logging code needs to be added to every</br>applicable method in the program. The logging code for each method may</br>be almost identical, creating an undesirable overlap in</br>functionality. Aspects let a programmer implement a cross-cutting</br>concern as a separate entity, through advice (how a concern should be</br>implemented) and join points (where it should be implemented). I will</br>give an introduction to aspect-orientation and aspect languages, and</br>also talk a bit about domain-specific aspect languages.it about domain-specific aspect languages.)
- Seminar/2009-03-25 + (Si une fonction φ promet de manipuler une … Si une fonction φ promet de manipuler une valeur de type α sans</br>l'observer, on peut utiliser son code sans risque pour toutes les</br>affectations possibles de α : que la valeur soit entière (α = int) ou</br>qu'elle soit un arbre (α = tree), la fonction se comportera</br>toujours de façon identique. Cette propriété s'appelle le polymorphisme</br>paramétrique, l'essence de la généricité.</br></br>Promettre de ne pas observer de trop près son argument est un fardeau</br>parfois insupportable pour une fonction, pour des raisons</br>algorithmiques (comment prendre une décision sans savoir ce que vaut</br>mon argument ?), ou encore pour des raisons de performances de</br>bas-niveau (si je sais que α = int, je peux utiliser une primitive</br>dédiée de mon processeur). Même si le type d'une valeur est caché</br>derrière un type plus abstrait α, on peut fournir des mécanismes pour</br>« le redécouvrir » grâce à des tests dynamiques ou à des raisonnements</br>purement statiques. La propriété qui permet de diriger son calcul par</br>la forme des types est appelée le polymorphisme intentionnel.</br></br>Dans cet exposé, nous présenterons plusieurs versions du</br>polymorphisme intentionnel offertes par différents systèmes de types</br>et de preuves sûrs (c'est-à-dire garantissant que les programmes</br>ne peuvent pas planter et sont corrects vis-à-vis de leur spécification).corrects vis-à-vis de leur spécification).)
- Seminar/2009-04-22 + (SmartEiffel, également connu sous le nom d … SmartEiffel, également connu sous le nom de GNU Eiffel, est à la fois</br>un langage et un ensemble d'outils de compilations, de documentation et</br>de validation.</br></br>Le langage SmartEiffel vise à favoriser la mise en pratique des</br>principales exigences liées au développement d'un gros logiciel par</br>une grande équipe. En plus d'exigences en terme de qualité, de</br>sécurité et de documentation, la définition de SmartEiffel est</br>également soucieuse de l'efficacité du programme à l'exécution. Ainsi,</br>le modèle des objets qui est à la base du langage intègre également</br>les types les plus élémentaires sans surcoût potentiel à l'exécution.</br>Pour sa part, le mécanisme de programmation par contrats qui est</br>essentiel en matière de documentation est également un bon moyen de</br>rechercher les meilleures performances à l'exécution.</br></br>Durant cet exposé, la visite guidée du langage présentera le modèle</br>d'objets, la programmation par contrats, la double forme d'héritage</br>multiple ainsi que le mécanisme des agents.ultiple ainsi que le mécanisme des agents.)
- Seminar/2019-10-01 + (The Loci Auto-Parallelizing framework prov … The Loci Auto-Parallelizing framework provides a Domain Specific</br>Language (DSL) for the creation of high performance numerical</br>models. The framework uses a logic-relation model to describe</br>irregular computations, provide guarantees of internal logical</br>consistency, and provides for automatic parallel execution. The</br>framework has been used to develop a number of advance computational</br>models used in production engineering processes. Currently Loci based</br>tools form the backbone of computational fluid dynamics tools used by</br>NASA Marshall and Loci based codes account for more than 20% of the</br>computational workload on NASA’s Pleiades supercomputer. This talk</br>will provide an overview of the framework, discuss its general</br>approach, and provide comparisons to other programming models through</br>a mini-app benchmark. In addition, future plans for developing</br>efficient schedules of fine-grained parallel and memory bandwidth</br>constrained computations will be discussed. Finally, some examples of</br>the range of engineering simulations enabled by the technology will be</br>introduced and briefly discussed. will be introduced and briefly discussed.)
- Seminar/2012-10-17 + (The Single-chip Cloud Computer (SCC) is a … The Single-chip Cloud Computer (SCC) is a 48-core experimental processor</br>created by Intel Labs targeting the many-core research community. The 6x4</br>mesh Network-on-Chip provides 24 tiles with 2 cores each. All cores are</br>independent and run their own instance of an operating system. It has</br>hardware support (local buffers on the tiles) for sending short messages</br>between cores, and allows for voltage and frequency control at 8 and 2 cores</br>respectively.</br></br>We have already modified the SVP runtime system to use these on-chip buffers</br>for the communication between threads executed on separate cores. We also</br>created a visual application for manual process migration and scheduling on</br>the SCC as well as a library for customized voltage and frequency scaling on</br>the chip.</br></br>Currently we focus on automated parallelization and mapping of one or</br>multiple sequential programs onto the 48 cores by modifying the daedalus</br>framework to target the SCC. The daedalus framework parallelizes sequential</br>C programs using Kahn Process Networks (KPNs) and generates code to run the</br>KPN on multiple hardware platforms like for example an FPGA, SMP CPU or</br>GPU. The SCC backend, which is work in progress, should result in a tool</br>that utilizes the SCC cores in an optimal way by means of performance and</br>energy consumption. It should also allow the system to dynamically adapt on</br>changes in the computational or communicational needs of the processes by</br>scaling frequency and migrating processes.scaling frequency and migrating processes.)
- Seminar/2011-11-16 + (The ilastik system developed by our group … The ilastik system developed by our group uses machine learning and</br>simple interaction techniques to empower users without special image</br>processing expertise to segment and analyze their 2- and 3-dimensional</br>image data on their own. It offers a number of easy-to-use workflows</br>for various common analysis tasks. The talk will present two of these</br>workflows (“interactive classification” and “region carving”), going</br>from an online demonstration of the high-level user experience down to</br>the algorithmic and software design details. Special emphasis will be</br>put on aspects of genericity and parallelization which facilitate</br>convenient adaptation of basic building blocks to different contexts</br>without loss of performance. Examples from challenging biological</br>applications will illustrate our system's capabilities.will illustrate our system's capabilities.)
- Seminar/2019-12-17 + (The relationship between neighboring pixel … The relationship between neighboring pixels plays an</br>important role in many vision applications. A typical example of a</br>relationship between neighboring pixels is the intensity order, which</br>gives rise to some morphological tree-based image representations</br>(e.g., Min/Max tree and tree of shapes). These trees have been shown</br>useful for many applications, ranging from image filtering to object</br>detection and segmentation. Yet, these intensity order based trees do</br>not always perform well for analyzing complex natural images. The</br>success of deep learning in many vision tasks motivates us to resort</br>to convolutional neural networks (CNNs) for learning such a</br>relationship instead of relying on the simple intensity order. As a</br>starting point, we propose the flux or direction field representation</br>that encodes the relationship between neighboring pixels. We then</br>leverage CNNs to learn such a representation and develop some</br>customized post-processings for several vision tasks, such as symmetry</br>detection, scene text detection, generic image segmentation, and crowd</br>counting by localization. This talk is based on [1] and [2], as well</br>as extension of those previous works that are currently under review.</br></br>[1] Xu, Y., Wang, Y., Zhou, W., Wang, Y., Yang, Z. and Bai, X.,</br>2019. Textfield: Learning a deep direction field for irregular scene</br>text detection. IEEE Transactions on Image Processing.</br>[2] Wang, Y., Xu, Y., Tsogkas, S., Bai, X., Dickinson, S. and Siddiqi,</br>K., 2019. DeepFlux for Skeletons in the Wild. In Proceedings of the</br>IEEE Conference on Computer Vision and Pattern Recognition.n Computer Vision and Pattern Recognition.)
- Seminar/2021-05-12 + (Topological Data Analysis (TDA) is a recen … Topological Data Analysis (TDA) is a recent area of computer science that focuses on discovering intrinsic structures hidden in data. Based on solid mathematical tools such as Morse theory and Persistent Homology, TDA enables the robust extraction of the main features of a data set into stable, concise, and multi-scale descriptors that facilitate data analysis and visualization. In this talk, I will give an intuitive overview of the main tools used in TDA (persistence diagrams, Reeb graphs, Morse-Smale complexes, etc.) with applications to concrete use cases in computational fluid dynamics, medical imaging, quantum chemistry, and climate modeling. This talk will be illustrated with results produced with the "Topology ToolKit" (TTK), an open-source library (BSD license) that we develop with collaborators to showcase our research. Tutorials for re-producing these experiments are available on the TTK website.eriments are available on the TTK website.)
- Seminar/2015-03-11 + (Motivé par de nombreuses applications, all … Motivé par de nombreuses applications, allant de la cryptographie au</br>calcul mathématique, le calcul formel s'est fortement développé ces</br>dernières années tant au niveau des algorithmes que des implantations</br>efficaces. L'efficacité des calculs repose sur celle de bibliothèques</br>dédiées, pour certaines opérations de base, comme l'algèbre linéaire</br>dans un corps fini ou avec des entiers multi-précision. Devant la</br>multiplicité des domaines de calcul et des variantes algorithmiques</br>disponibles, la conception de ces bibliothèques doit concilier une</br>forte généricité avec l'efficacité.</br></br>Nous allons présenter comment cette problématique est abordée dans les</br>bibliothèques d'algèbre linéaire exacte FFLAS-FFPACK (2) et LinBox</br>(3). Après une présentation générale de ces projets, nous focaliserons</br>la présentation sur trois aspects représentatifs:</br></br>- l'exploitation des diverses arithmétiques de base (entière,</br>flottante, booléenne), de routines numériques optimisées et leur</br>intégration au sein d'algorithmes génériques haut niveau ;</br></br>- l'approche boîte-noire de la bibliothèque LinBox, proposant un</br>modèle algorithmique spécifique, particulièrement performant pour les</br>matrices creuses ou structurées ;</br></br>- La parallélisation de code dans FFLAS-FFPACK, basée sur un langage</br>spécifique (DSL) permettant d'utiliser de façon interchangeable</br>différents langages et moteurs exécutifs, et de tirer parti du</br>parallélisme de tâche avec dépendance par flot de données.tâche avec dépendance par flot de données.)
- Seminar/2016-09-28 + (Traditionnellement, la prospection commerc … Traditionnellement, la prospection commerciale B2B se fait grâce à des</br>listes d'entreprises classées manuellement, sur la base de données</br>administratives renseignées à la création des entreprises. Ces listes</br>sont donc souvent dépassées, très chères et peu qualifiées.</br></br>C-Radar, produit développé par la société Data Publica, veut</br>transformer la prospection commerciale en enrichissant ces données</br>administratives par des données issues du web. Ainsi, on obtient des</br>données fraîches, plus ciblées. Et grâce aux techniques de machine</br>learning et de clustering, on peut obtenir automatiquement des listes</br>d'entreprises pertinentes à faible coût.</br></br>Lors de cette présentation, nous aborderons les différentes techniques</br>de science des données mises en œuvre dans ce produit, en relation</br>avec les fonctionnalités du produit.ation avec les fonctionnalités du produit.)
- Seminar/2012-03-21 + (Une question fondamentale pour mes recherc … Une question fondamentale pour mes recherches est de savoir ce qu'est</br>une image. Cela peut sembler à première vue une question trop simple :</br>une image, c'est un ensemble de points. Mais ces points sont reliés</br>entre eux, c'est ce qu'on appelle une structure, et ils ont des</br>données de types multiples qui leur sont attachées. La bibliothèque</br>Milena, développée au LRDE, est une bibliothèque générique dédiée au</br>traitement d'images. Dans Milena, trois axes indépendants sont</br>développés : l'axe des structures, l'axe des données, et celui des</br>algorithmes, c'est-à-dire de ce qu'on peut faire avec une image.</br></br>Dans cet exposé, je vais développer plusieurs exemples dans lesquels</br>je choisirai un algorithme et un type de données, en faisant varier la</br>structure. Changer la structure, c'est penser les images d'une manière</br>différente, et c'est quelque chose d'extrêmement porteur en recherche.</br></br>- Un premier exemple est celui d'un algorithme classique de</br> segmentation : la ligne de partage des eaux. Originellement pensé sur</br> les pixels, sa traduction dans le cadre des arêtes donne le problème</br> classique d'arbre couvrant de poids minimum. Si la ligne de partage</br> des eaux est très connue en traitement d'images, les arbres de</br> poids minimum sont très utilisés en classification. Un pont naturel</br> est alors établi entre deux communautés différentes, et les idées</br> provenant de ces deux communautés peuvent être combinées.</br></br>- Un deuxième exemple est celui de la représentation arborescente des</br> images. Pour illustrer, tant les lignes de niveaux que les</br> composantes connexes des ensembles de niveaux (les coupes) des</br> images sont naturellement structurées en arbre : deux lignes ou deux</br> composantes sont soit disjointes soit emboîtées. On peut filtrer</br> une image en éliminant de l'arbre tous les nœuds qui ne vérifient</br> pas un critère. Mais on peut aussi considérer l'arbre lui-même comme</br> une image, et appliquer sur cet arbre un algorithme de traitement</br> d'images. C'est une idée récursive très riche.</br></br>D'autres exemples pourront être développés en fonction du temps : liens</br>entre ligne de partage des eaux topologique et segmentation</br>hiérarchique, topologie discrète dans divers cadres...</br></br>La bibliothèque Milena permet d’appliquer la plupart des algorithmes</br>existants à une nouvelle structure, ce qui est un gain de temps</br>incontestable. Cela permet de se concentrer sur ce qui fait le cœur</br>de mon métier: chercher un algorithme plus efficace, adapté à un type</br>de structure, ou encore chercher quelles sont les propriétés</br>mathématiques d’un algorithme sur une structure donnée. d’un algorithme sur une structure donnée.)
- Seminar/2017-02-08 + (Vcsn est une plateforme consacrée aux auto … Vcsn est une plateforme consacrée aux automates et aux expressions</br>rationnelles. Parce qu'elle traite une large variété de natures</br>d'automates, elle place en son coeur le concept de "contexte", qui</br>type les automates, les expressions rationnelles, etc. La plateforme</br>repose sur une bibliothèque C++14 "templatée" par des contextes, au</br>dessus de laquelle la couche "dyn" qui, grâce à de l'effacement de</br>type et de la compilation à la volée, offre à l'utilisateur le confort</br>d'une bibliothèque traditionnelle avec la généricité et les</br>performances d'une bibliothèque templatée. Ces bibliothèques sont</br>ensuite exposées au travers d'outils en ligne de commande, mais aussi</br>Python et surtout IPython, qui permettent une exploration interactive</br>simple d'algorithmes.</br>La bibliothèque Vcsn repose sur un ensemble d'objets - automates,</br>étiquettes, poids, polynômes, expressions rationnelles et</br>développements rationnels - sur lesquels sont fournis plus de trois</br>cents algorithmes. Dans certains cas, Vcsn offre des fonctionalités</br>inégalées, et certains de ces algorithmes ont des performances</br>supérieures à celles des projets comparables.</br></br>Nous ferons une présentation de l'architecture générale de Vcsn, sous</br>la forme d'une démonstration guidée par les questions, ainsi qu'un</br>exposé des objectifs de Vcsn 3.0.si qu'un exposé des objectifs de Vcsn 3.0.)
- Seminar/2021-02-10 + (We introduce iposets - posets with interfa … We introduce iposets - posets with interfaces - equipped with a novel gluing</br>composition along interfaces and the standard parallel composition. We study</br>their basic algebraic properties as well as the hierarchy of gluing-parallel</br>posets generated from singletons by finitary applications of the two</br>compositions. We show that not only series-parallel posets, but also</br>interval orders, which seem more interesting for modeling concurrent and</br>distributed systems, can be generated, but not all posets. Generating posets</br>is also important for constructing free algebras for concurrent semi-rings</br>and Kleene algebras that allow compositional reasoning about such systems.ompositional reasoning about such systems.)
- Seminar/2022-06-22 + (We present a framework for modelling and v … We present a framework for modelling and verifying epistemic properties over</br>parameterized multi-agent systems that communicate by truthful public</br>announcements. In this framework, the number of agents or the amount of certain</br>resources are parameterized (i.e. not known a priori), and the corresponding</br>verification problem asks whether a given epistemic property is true regardless</br>of the instantiation of the parameters. As in other regular model checking (RMC)</br>techniques, a finite-state automaton is used to specify a parameterized family</br>of systems.</br></br>Parameterized systems might also require an arbitrary number of announcements,</br>leading to the introduction of the so-called iterated public announcement.</br>Although model checking becomes undecidable because of this operator, we provide</br>a semi-decision procedure based on Angluin's L*-algorithm for learning finite</br>automata. Moreover, the procedure is guaranteed to terminate when some</br>regularity properties are met. We illustrate the approach on the Muddy Children</br>puzzle, and we further discuss dynamic protocol encodings through the Dining</br>Cryptographer example.</br></br>Initial publication at AAMAS21, joint work with Anthony Lin and Felix Thomasint work with Anthony Lin and Felix Thomas)
- Seminar/2018-05-30 + (We show a symbolic-execution-based algorit … We show a symbolic-execution-based algorithm computing the precise</br>effect of a program cycle on program variables. For a program variable,</br>the algorithm produces an expression representing the variable value</br>after the number of cycle iterations specified by parameters of the</br>expression. The algorithm is partial in the sense that it can fail to</br>find such an expression for some program variables (for example, it</br>fails in cases where the variable value depends on the order of paths in</br>the cycle taken during iterations).</br></br>We present two applications of this loop summarization procedure. The</br>first is the construction of a nontrivial necessary condition on program</br>input to reach a given program location. The second application is a</br>loop bound detection algorithm, which produces tighter loop bounds than</br>other approaches.tighter loop bounds than other approaches.)
- Seminar/2008-04-30 + (Mouldable programming is about looking at … Mouldable programming is about looking at programs as mouldable</br>fragments of code, not as the static, brittle syntax software often</br>turns out to be. Some simple examples follow. The notation for calling</br>a method "push" which adds an element "E" to a stack "S" can be OO or</br>static method style, it can modify "S" or return the new stack</br>etc. Can we simplify usage to just one form, and mould it to the</br>actual call? A function which breaks down for some input can signal</br>this using return flags, special return values, or exceptions, to name</br>some common ways. Can we abstract over this, and mould to the relevant</br>error handling technique? Often we need to do run-time checking of</br>arguments, e.g., array indexing bounds, forcing us to introduce lots</br>of code to deal with the unwanted cases. Can we use mouldable ideas to</br>simplify the code? In the presentation, we will elaborate on such</br>examples, discussing how we can free us from awkward syntactic</br>constraints.ree us from awkward syntactic constraints.)
- Seminar/2012-02-15 + («The effective exploitation of his powers … «The effective exploitation of his powers of abstraction must be</br>regarded as one of the most vital activities of a competent</br>programmer.» disait Dijsktra.</br></br>En effet, pour aborder la complexité d'un problème, l'explicitation</br>des concepts utiles à sa formalisation et à sa résolution est bien</br>souvent une étape clé. Lorsque que l'on étend ce processus à une</br>classe de problèmes qui partagent les mêmes concepts, il est naturel</br>de se doter d'un langage le plus approprié possible pour manipuler ces</br>abstractions spécifiques à un domaine (en anglais, «Domain Specific</br>Language»).</br></br>Comment implémenter ces DSLs? Une première approche classique reflète</br>les constructions du DSL sous la forme d'un jeu de fonctions de</br>bibliothèque. L'avantage de cette approche est d'utiliser directement</br>son langage généraliste préféré, et sa chaîne de compilation</br>optimisée, de façon à générer du code machine à moindre frais. Par</br>contre, dans ce cadre, l'écriture de passe d'optimisations spécifiques</br>au DSL - à moins d'utiliser des techniques pointues de</br>méta-programmation - est a priori impossible.</br></br>Une seconde approche, opposée, consiste à écrire un compilateur pour</br>le DSL à partir de zéro. Toute liberté est alors donnée à</br>l'implémenteur d'intégrer à son compilateur des passes d'optimisation</br>spécifiques… mais au prix d'une réimplémentation de passes de</br>compilation déjà présentes, et certainement plus abouties, dans le</br>compilateur de son langage généraliste favori.</br></br>Dans cet exposé, je présenterai les travaux de Martin Odersky et</br>son équipe sur la virtualisation de DSLs à l'intérieur du langage de</br>programmation Scala. La virtualisation de langage utilise</br>intensivement le polymorphisme et la composition mixin de Scala ainsi</br>que des techniques de génération de code à l'exécution pour embarquer</br>des langages spécifiques dans Scala dont la compilation peut</br>réutiliser des modules du compilateur mais aussi étendre ces derniers</br>par des optimisations spécifiques au domaine. des optimisations spécifiques au domaine.)