Annonce

annonce@lrde.epita.fr

564 discussions

Prochain séminaire MeFoSyLoMa : vendredi 8 avril 2016 au LRDE (Epita)

by Alexandre Duret-Lutz

Bonjour à tous, La prochaine séance du séminaire MeFoSyLoMa sera orientée outils, et se tiendra au LRDE. ======================================================================== Séminaire MeFoSyLoMa http://www.mefosyloma.fr/ Méthodes Formelles pour Les Systèmes Logiciels et Matériels Vendredi 8 avril 2016, 14h-17h Adresse: LRDE (Epita), Salle Alpha Bâtiment X, 2e étage 18 rue Pasteur, 94270 Le Kremlin-Bicêtre Métro Porte d'Italie Plans d'accès : https://www.google.com/maps?q=48.8152808,2.3623765 https://www.lrde.epita.fr/~adl/dl/acces-lrde.pdf S'il y en a parmi vous qui comptent venir en voiture, le parking du centre commercial Okabé est gratuit pendant 3h. http://www.okabe.com/okabe/fr/okabe-parking ======================================================================== Le séminaire MeFoSyLoMa est animé conjointement par les laboratoires Cedric (Cnam), IBISC (Univ. Evry), LACL (Univ. Paris 12), LIP6 (UPMC), LIPN (Univ. Paris 13), LRDE (Epita), LSV (École Normale Supérieure de Cachan) et LTCI (TELECOM ParisTech). Son objet est de permettre la confrontation de différentes approches ou points de vue sur l'utilisation des méthodes formelles dans les domaines du génie logiciel, de la conception de circuit, des systèmes répartis, des systèmes temps-réel ou encore des systèmes d'information. Il s'organise autour de réunions bimestrielles où sont exposés des travaux de recherche récents sur ce thème. ======================================================================== Programme 14h00-14h45: Alexandre Duret-Lutz (LRDE/Epita) Spot 2.0 Je présenterai Spot 2.0, une bibliothèque C++ de manipulation d'omega-automates pour le model checking. Les nouveautés sont assez nombreuses: la bibliothèque travaille maintenant avec des automates dont la condition d'acceptation peut être arbitrairement complexe (par exemple une combinaison booléenne de Streett et Rabin généralisé), de nouveaux outils en ligne de commande permettent de manipuler et produire ces automates, et la majeur partie des fonctionnalités est utilisable avec une surcouche de bindings pour Python. Je montrerai en particulier: - des exemples d'utilisation tirés du cours d'initiation au model checking de l'Epita (travail sur la sémantique de LTL, et écriture d'un model checker jouet en quelques lignes de Python). - la facilité avec laquelle on peut chaîner les différents outils pour construire un pipeline de manipulation d'automates - une technique utilisant un SAT-solver pour synthétiser des automates équivalents mais avec d'autres conditions d'acceptation. 14h45-15h30: Maximilien Colange (ENS de Cachan) Je présenterai TiAMo, un model-checker pour les systèmes temporisés développé au LSV. Les systèmes temporisés présentent une composante en temps continu, qui font de leurs espaces d'états des graphes infinis à branchement infini. Dans le cadre du model-checking, leur analyse repose essentiellement sur des abstractions permettant de se ramener à des graphes discrets. Nous nous concentrons sur les problèmes d'accessibilité dans les automates temporisés, et d'accessibilité optimale dans les automates temporisés à coûts positifs. TiAMo est pensé comme une plateforme permettant la comparaison expérimentale des différents algorithmes et abstractions pour la vérification de systèmes temporisés. Je rappellerai les principaux problèmes algorithmiques qui se posent dans ce cadre, et les différentes solutions qui ont été proposées. Je présenterai également l'outil TiAMo, et les algorithmes d'analyse qu'il implémente. 15h30-16h00: pause café 16h00: vie du groupe ======================================================================== -- Alexandre Duret-Lutz

9 years

New journal publication: TextCatcher: a method to detect curved and challenging text in natural scenes (IJDAR)

by Jonathan Fabrizio

We are happy to announce that the following paper has been accepted for publication in the International Journal of Document Analysis and Recognition (IJDAR): TextCatcher: a method to detect curved and challenging text in natural scenes Jonathan Fabrizio (1) Myriam Robert-Seidowsky (1) Séverine Dubuisson (2) Stefania Calarasanu (1) Raphaël Boissel (1) (1) EPITA Research and Development Laboratory (LRDE) (2) Sorbonne Universités, UPMC - ISIR In this paper, we propose a text detection algorithm which is hybrid and multi-scale. First, it relies on a connected component-based approach: After the segmentation of the image, a classification step using a new wavelet descriptor spots the letters. A new graph modeling and its traversal procedure allow to form candidate text areas. Second, a texture-based approach discards the false positives. Finally, the detected text areas are precisely cut out and a new binarization step is introduced. The main advantage of our method is that few assumptions are put forward. Thus, “challenging texts” like multi-sized, multi-colored, multi- oriented or curved text can be localized. The efficiency of TextCatcher has been validated on three different datasets: Two come from the ICDAR competition, and the third one contains photographs we have taken with various daily life texts. We present both qualitative and quantitative results.

9 years, 1 month

[Seminaire-LRDE] Mercredi 23 mars 2016: Joël Falcou, Université Paris Sud, NumScale

by Daniela Becker

Chers collègues, En mars, nous vous invitons à une deuxième session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) après celle de demain Mercredi 16 mars, où nous recevons Guillaume Torchon, Grenoble-INP & GIPSA-lab, pour parler d’"Analyse hiérarchique d’images multimodales ». Vous pouvez dès à présent noter le 2e rendez-vous du LRDE : Mercredi 23 mars 2016 (11h--12h), Salle L0 du LRDE. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2016-03-23 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 23 mars 2016 : * 11h: Boost.SIMD - Maximisez votre CPU directement depuis C++ -- Joël Falcou, Université Paris Sud, NumScale https://github.com/NumScale/boost.simd Les extensions multimédia (SSE, AVX, NEON) sont une composante majeure des processeurs d'aujourd'hui qui restent plus que sous-utilisées. Les principales raisons de cette sous-utilisation sont la relative obscurité des jeux d'instructions, leur variété entre et même au sein des différentes familles de puces et surtout, une méconnaissance de la disponibilité des ces unités de calculs. Boost.SIMD est une bibliothèque permettant d'exploiter ces extensions de manière efficace et expressive, facilitant l'utilisation, la diffusion et la portabilité de tels codes, ouvrant la porte à des accélérations de l'ordre de 4 à 10 sur un simple cœur. Cet exposé présentera les fonctionnalités de Boost.SIMD, les challenges posés par son implémentation, comment le C++ moderne répond à plusieurs de ces problèmes et les éléments bloquants qu'il reste à résoudre. -- Joël Falcou est maître de conférences en informatique au LRI, Université Paris Sud. Ses travaux de thèse ont porté sur la programmation parallèle pour la vision artificielle et plus particulièrement sur les applications de la programmation générative pour la création d'outils d'aide à la parallélisation. Il est également conseiller scientifique chez NumScale. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d’orateurs. -- Akim Demaille Akim.Demaille(a)lrde.epita.fr _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

9 years, 1 month

[Seminaire-LRDE] Mercredi 16 mars 2016: Guillaume Tochon - Grenoble-INP & GIPSA-lab

by Daniela Becker

Chers collègues, La prochaine session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) aura lieu le Mercredi 16 mars 2016 (11h--12h), Salle L0 du LRDE. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2016-03-16 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 16 mars 2016 : * 11h: Analyse hiérarchique d'images multimodales -- Guillaume Tochon - Grenoble-INP & GIPSA-lab Il y a un intérêt grandissant pour le développement d’outils de traitements adaptés aux images multimodales (plusieurs images de la même scène acquises avec différentes caractéristiques). Permettant une représentation plus complète de la scène en question, ces images multimodales ont de l'intérêt dans plusieurs domaines du traitement d'images. Les exploiter et les manipuler de manière optimale soulève cependant plusieurs questions. Dans cet exposé, nous étendrons les représentations hiérarchiques, outil puissant pour le traitement et l’analyse d’images classiques, aux images multimodales afin de mieux exploiter l’information additionnelle apportée par la multimodalité et améliorer les techniques classiques de traitement d’images. En particulier, nous nous concentrerons principalement sur deux modalités différentes, fréquemment rencontrées dans le domaine de la télédétection: - La modalité spectrale-spatiale, propre aux images hyperspectrales (images à très haute résolution spectrale - plusieurs centaines de canaux). Une intégration adaptée de cette information spectrale-spatiale lors de l'étape de construction de la représentation hiérarchique (en l’occurrence, un arbre de partition binaire) nous permettra par la suite, via un processus de minimisation énergétique, de proposer une carte de segmentation de l'image optimale vis-à-vis de l'opération de démélange spectral. - La modalité sensorielle, c'est-à-dire les images acquises par des capteurs de différentes natures. Ces images "multisources", porteuses d'informations à la fois redondantes et complémentaires, sont particulièrement intéressantes pour des applications de segmentation. Nous proposerons une méthode se basant sur le très récent concept de tresses de partitions (extensions des hiérarchies de partitions classiques) afin de réaliser l'analyse hiérarchique de ces images multisources, et en obtiendrons une segmentation (là encore) via un processus de minimisation énergétique. - Enfin, nous décrirons très brièvement une méthode d'analyse d'images multitemporelles permettant d'effectuer du suivi d'objet, en se basant également sur les représentations hiérarchiques des différentes images de la séquence. -- Guillaume Tochon a obtenu un diplôme d'ingénieur de Grenoble-INP (école ENSE3) en 2012 et un doctorat de l'université de Grenoble Alpes (rattaché au laboratoire GIPSA-lab) en 2015, tous deux en spécialisation ``traitement du signal et des images''. Il est actuellement attaché temporaire d'enseignement et de recherche à Grenoble-INP et conduit ses recherches au sein du département Images et Signaux du GIPSA-lab. Ses activités de recherches se situent à l'intersection entre la morphologie mathématique et la fusion de données, se focalisant notamment sur l'utilisation de représentations hiérarchiques pour l'analyse d'images multimodales, pour diverses applications telles que la segmentation ou le démélange spectral. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d’orateurs. -- Akim Demaille Akim.Demaille(a)lrde.epita.fr _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

9 years, 1 month

ACCU 2016 session

by Didier Verna

I am pleased to announce that I will hold a 90' session at the next ACCU conference in Bristol, next April. The abstract is given below. A Taste of Julia Julia is a recent programming language developed at MIT and sold as a high level, high performance dynamic language for scientific computing. One of the co-authors of Julia has a Scheme background, and in fact, it appears that Julia borrows a lot from Scheme, Common Lisp and Dylan. This is to the point that Julia may even be considered as a new Lisp dialect. This is enough, already, to catch our attention, but there's more. Julia also seems to benefit from modern optimization techniques for dynamic languages, notably through its LLVM based JIT compiler. In this talk, we will give a tour of the language's most prominent features, with a slight focus on what makes it a Lisp, sometimes (not always) an even better one that the existing alternatives. -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

9 years, 2 months

[CfP] ELS 2016 Deadline extension: Sat Feb 27

by Didier Verna

ELS'16 - 9th European Lisp Symposium Department of Computer Science AGH University of Science and Technology Kraków, Poland May 9-10, 2016 In cooperation with: ACM SIGPLAN Sponsored by EPITA, Franz Inc., LispWorks Ltd., IdEx and Dept. of Computer Science AGH UST http://www.european-lisp-symposium.org/ Recent news: - *** Submission deadline extended to Saturday Feb 27 *** The purpose of the European Lisp Symposium is to provide a forum for the discussion and dissemination of all aspects of design, implementation and application of any of the Lisp and Lisp-inspired dialects, including Common Lisp, Scheme, Emacs Lisp, AutoLisp, ISLISP, Dylan, Clojure, ACL2, ECMAScript, Racket, SKILL, Hop and so on. We encourage everyone interested in Lisp to participate. The 9th European Lisp Symposium invites high quality papers about novel research results, insights and lessons learned from practical applications and educational perspectives. We also encourage submissions about known ideas as long as they are presented in a new setting and/or in a highly elegant way. Topics include but are not limited to: - Context-, aspect-, domain-oriented and generative programming - Macro-, reflective-, meta- and/or rule-based development approaches - Language design and implementation - Language integration, inter-operation and deployment - Development methodologies, support and environments - Educational approaches and perspectives - Experience reports and case studies We invite submissions in the following forms: Papers: Technical papers of up to 8 pages that describe original results or explain known ideas in new and elegant ways. Demonstrations: Abstracts of up to 2 pages for demonstrations of tools, libraries, and applications. Tutorials: Abstracts of up to 4 pages for in-depth presentations about topics of special interest for at least 90 minutes and up to 180 minutes. The symposium will also provide slots for lightning talks, to be registered on-site every day. All submissions should be formatted following the ACM SIGS guidelines and include ACM classification categories and terms. For more information on the submission guidelines and the ACM keywords, see: http://www.acm.org/sigs/publications/proceedings-templates and http://www.acm.org/about/class/1998. The conference proceedings will be published in the ACM Digital Library. Important dates: - *** EXTENDED *** 27 Feb 2016 Submission deadline *** EXTENDED *** - 25 Mar 2016 Notification of acceptance - 15 Apr 2016 Early registration deadline - 22 Apr 2016 Final papers due - 9-10 May 2016 Symposium Programme chair: Irène Durand, LaBRI, University of Bordeaux, France Local chair: Michał Psota, Emergent Network Defense, Kraków, Poland Programme committee: Antonio Leitao — INESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Portugal Charlotte Heerzel — IMEC, Leuven, Belgium Christian Queinnec — University Pierre et Marie Curie, Paris 6, France Christophe Rhodes — Goldsmiths, University of London, United Kingdom Didier Verna — EPITA Research and Development Laboratory, France Erick Gallesio — University of Nice-Sophia Antipolis, France François-René Rideau, Google, USA Giuseppe Attardi — University of Pisa, Italy Henry Lieberman — MIT, USA Kent Pitman, HyperMeta Inc., USA Leonie Dreschler-Fischer — University of Hamburg, Germany Pascal Costanza — Intel Corporation, Belgium Robert Strandh — University of Bordeaux, France Search Keywords: #els2016, ELS 2016, ELS '16, European Lisp Symposium 2016, European Lisp Symposium '16, 9th ELS, 9th European Lisp Symposium, European Lisp Conference 2016, European Lisp Conference '16 -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

9 years, 2 months

Vcsn 2.2 is released!

by Akim Demaille

We are very happy to announce the release of Vcsn 2.2! This version, code-named "the lazy release", concludes the work from Antoine and Valentin, who left EPITA for their final internship. In addition to the usual load of improvements (more doc and less bugs), this version features some noteworthy changes: - several algorithms now offer a lazy variant: compose, conjunction, derived_term, determinize, insplit, and proper. Instead of completing the construction on invocation, the result is built incrementally, on demand, e.g., when requested by an evaluation. This is especially useful for large computations a fraction of which is actually needed (e.g., composition of two large automata and then with a small one), or for computations that would not terminate (e.g., determinization of some weighted automata). - the functions `automaton.lightest` and `automaton.lightest_automaton` explore the computations (i.e., paths of accepted words) with the smallest weights (dubbed "shortest paths" for tropical-min semirings). They feature several implementations controlled via the `algo` argument. - rational expressions now support UTF-8 operators in input and output. They also learned a few tricks to be better looking (e.g., `aaa` => `a³`). - several new algorithms or improvements or generalizations of existing ones. - a number of performance improvements. More details are available on Vcsn’s web site. People who worked on this release: - Akim Demaille - Antoine Pietri - Lucien Boillod - Nicolas Barray - Raoul Billion - Sébastien Piat - Thibaud Michaud - Valentin Tolmer People who have influenced this release: - Alexandre Duret-Lutz - Jacques Sakarovitch - Luca Saiu Vcsn 2.2: http://vcsn.lrde.epita.fr/Vcsn2.2 Everything about Vcsn: http://vcsn.lrde.epita.fr Online Vcsn: http://vcsn-sandbox.lrde.epita.fr

9 years, 2 months

[Seminaire-LRDE] Mercredi 17 février 2016: Stephan Hadinger, Head of Solutions Architecture, AWS

by Daniela Becker

Chers collègues, La prochaine session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) aura lieu le Mercredi 17 février 2016 (11h--12h), Salle L0 du LRDE. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2016-02-17 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 17 février 2016 : * 11h: Computing with (nearly) unlimited resources -- Stephan Hadinger, Head of Solutions Architecture, AWS https://aws.amazon.com Le cloud computing donne accès à des ressources de stockage et de calcul quasiment illimitées, pour un coût toujours plus bas. Devant l’explosion de la quantité des données générées et le besoin de réagir toujours plus vite, il n’a jamais été aussi facile d’accéder aux technologies de traitement massif. Nous illustrerons de nombreux cas d’usage du cloud : Hadoop, dataware-house de plusieurs Po, traitement temps réel de millions d’événements par seconde, IOT, Machine Learning… En particulier, l’utilisation d’algorithmes massivement parallèles prend toute son importance et permet de tirer pleinement parti de l’élasticité du cloud, par exemple: Monte-Carlo dans le domaine financier, modélisation de protéines en 3D pour du screening, analyse génomique, analyse de logs… -- Stephan Hadinger a fait une longue carrière dans l'IT, spécialisé dans les domaines Infrastructure, B2C et B2B afin de permettre aux entreprises de tirer un maximum de bénéfices de leurs investissements technologiques. Dans son rôle d'Architecte Solutions avec Amazon Web Services, Stephan travaille avec des entreprises françaises de toutes tailles pour les aider à migrer vers le Cloud et utiliser leur IT pour mieux servir leurs clients. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d’orateurs. -- Akim Demaille Akim.Demaille(a)lrde.epita.fr _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

9 years, 2 months

[CfP] 9th European Lisp Symposium, May 9-10, Krakow, Poland

by Didier Verna

ELS'16 - 9th European Lisp Symposium Department of Computer Science AGH University of Science and Technology Kraków, Poland May 9-10, 2016 In cooperation with: ACM SIGPLAN Sponsored by EPITA, Franz Inc., LispWorks Ltd. and Dept. of Computer Science AGH UST http://www.european-lisp-symposium.org/ Recent news: - Submission deadline in less than a month! - 3nd invited speaker announced: Stephan Karpinski on Julia: to Lisp or Not to Lisp? The purpose of the European Lisp Symposium is to provide a forum for the discussion and dissemination of all aspects of design, implementation and application of any of the Lisp and Lisp-inspired dialects, including Common Lisp, Scheme, Emacs Lisp, AutoLisp, ISLISP, Dylan, Clojure, ACL2, ECMAScript, Racket, SKILL, Hop and so on. We encourage everyone interested in Lisp to participate. The 9th European Lisp Symposium invites high quality papers about novel research results, insights and lessons learned from practical applications and educational perspectives. We also encourage submissions about known ideas as long as they are presented in a new setting and/or in a highly elegant way. Topics include but are not limited to: - Context-, aspect-, domain-oriented and generative programming - Macro-, reflective-, meta- and/or rule-based development approaches - Language design and implementation - Language integration, inter-operation and deployment - Development methodologies, support and environments - Educational approaches and perspectives - Experience reports and case studies We invite submissions in the following forms: Papers: Technical papers of up to 8 pages that describe original results or explain known ideas in new and elegant ways. Demonstrations: Abstracts of up to 2 pages for demonstrations of tools, libraries, and applications. Tutorials: Abstracts of up to 4 pages for in-depth presentations about topics of special interest for at least 90 minutes and up to 180 minutes. The symposium will also provide slots for lightning talks, to be registered on-site every day. All submissions should be formatted following the ACM SIGS guidelines and include ACM classification categories and terms. For more information on the submission guidelines and the ACM keywords, see: http://www.acm.org/sigs/publications/proceedings-templates and http://www.acm.org/about/class/1998. The conference proceedings will be published in the ACM Digital Library. Important dates: - 19 Feb 2016 Submission deadline - 25 Mar 2016 Notification of acceptance - 15 Apr 2016 Early registration deadline - 22 Apr 2016 Final papers due - 9-10 May 2016 Symposium Programme chair: Irène Durand, LaBRI, University of Bordeaux, France Local chair: Michał Psota, Emergent Network Defense, Kraków, Poland Programme committee: Antonio Leitao — INESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Portugal Charlotte Heerzel — IMEC, Leuven, Belgium Christian Queinnec — University Pierre et Marie Curie, Paris 6, France Christophe Rhodes — Goldsmiths, University of London, United Kingdom Didier Verna — EPITA Research and Development Laboratory, France Erick Gallesio — University of Nice-Sophia Antipolis, France François-René Rideau, Google, USA Giuseppe Attardi — University of Pisa, Italy Henry Lieberman — MIT, USA Kent Pitman, HyperMeta Inc., USA Leonie Dreschler-Fischer — University of Hamburg, Germany Pascal Costanza — Intel Corporation, Belgium Robert Strandh — University of Bordeaux, France Search Keywords: #els2016, ELS 2016, ELS '16, European Lisp Symposium 2016, European Lisp Symposium '16, 9th ELS, 9th European Lisp Symposium, European Lisp Conference 2016, European Lisp Conference '16 -- @-quartet live: Sunset/Sunside, Paris, Jan 26 2016 ! Book now: http://www.sunset-sunside.com/2016/1/artiste/2101/3453/ Lisp, Jazz, Aïkido: http://www.didierverna.info

9 years, 3 months

[Seminaire-LRDE] Subject: Mercredi 27 janvier 2016: Pierre-Yves Strub -- IMDEA Software Institute - Espagne

by Daniela Becker

Chers collègues, La prochaine session du séminaire Performance et Généricité du LRDE (Laboratoire de Recherche et Développement de l'EPITA) aura lieu le Mercredi 27 janvier 2016 (11h--12h), Salle L0 du LRDE. Vous trouverez sur le site du séminaire [1] les prochaines séances, les résumés, captations vidéos et planches des exposés précédents [2], le détail de cette séance [3] ainsi que le plan d'accès [4]. [1] http://seminaire.lrde.epita.fr [2] http://seminaire.lrde.epita.fr/Archives [3] http://seminaire.lrde.epita.fr/2016-01-27 [4] http://www.lrde.epita.fr/Contact Au programme du Mercredi 27 janvier 2016 : * 11h: Une introduction à la preuve formelle de sécurité -- Pierre-Yves Strub -- IMDEA Software Institute - Espagne http://www.strub.nu La cryptographie joue un rôle clé dans la sécurité des infrastructures de communication. Il est donc d'une importance capitale de construire des systèmes cryptographiques apportant de fortes garanties de sécurité. C'est dans ce but que les constructions cryptographiques sont étudiées scrupuleusement et viennent avec une preuve de sécurité bornant la probabilité qu'un adversaire casse le crypto-système. La majorité des preuves de sécurité sont réductionnistes: elles construisent, à partir d'un adversaire PPT (Probabilistic Polynomial-Time) violant avec une probabilité écrasante la sécurité de la construction cryptographique, un second adversaire PPT cassant une hypothèse de sécurité. Cette approche, connue sous le nom de "sécurité formelle", permet sur le principe de fournir des preuves mathématiques rigoureuses et détaillées de sécurité. Les récentes constructions cryptographiques (et donc leur analyse de sécurité) sont de plus en plus complexes, et il n'est pas rare qu'elles incluent maintenant la preuve sécurité de l'implémentation du crypto-système, ou de sa résistance aux canaux cachés. En conséquence, les preuves de sécurité de ces algorithmes présentent un niveau de complexité tel qu'un grand nombre d'entre elles sont fausses --- prouvant la sécurité d'une construction qui ne l'est pas. Une solution prometteuse pour pallier ce problème est de développer des outils formels d'aide à la construction et vérification de crypto-systèmes. Bien que de nombreux outils existent pour la cryptographie symbolique, peu d'effort a été fait pour la cryptographie calculatoire --- pourtant utilisée largement parmi les cryptographes. Après avoir introduit le domaine de la preuve formelle et de la sécurité formelle, je présenterai EasyCrypt, un outil d'aide à la preuve des constructions cryptographiques dans le modèle calculatoire. EasyCrypt adopte une approche reposant sur la formalisation de constructions cryptographiques à partir de code concret, dans laquelle la sécurité et les hypothèses de sécurité sont modélisées à partir de programmes probabilistes et où les adversaires sont représentés par du code non spécifié. Une telle approche permet l'utilisation d'outils existants pour la vérification de programmes. EasyCrypt est développé conjointement entre l'IMDEA Software Institute et Inria. -- Pierre-Yves Strub est chercheur au "IMDEA Software Institute", institut madrilène de recherche en informatique. En 2008, il obtient une thèse en informatique de l'École Polytechnique, puis rejoint l'équipe FORMES du laboratoire commun INRIA-Tsinghua University (Pékin, Chine). Avant d'intégrer IMDEA en 2012, il passe deux ans au laboratoire commun MSR-INRIA (Paris, France). Ses recherches portent sur les méthodes formelles, la logique en informatique, la vérification de programmes, la sécurité formelle et la formalisation des mathématiques. -- Depuis qu'il a rejoint IMDEA, ses recherches portent principalement sur la preuve formelle assistée par ordinateur en sécurité/cryptographie. Il est l'un des principaux concepteur et développeur d'EasyCrypt, un outil dédié à la preuve de sécurité de constructions cryptographiques. L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette information le plus largement possible. N'hésitez pas à nous faire parvenir vos suggestions d’orateurs. -- Akim Demaille Akim.Demaille(a)lrde.epita.fr _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

9 years, 3 months

← Newer
1
...
17
18
19
20
21
22
23
...
57
Older →

Jump to page:

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Annonce