Annonce

annonce@lrde.epita.fr

565 discussions

by Renault Etienne

Greetings, We are pleased to announce that the following paper has been accepted in the 12th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS'18). Please find the title and abstract below. Title and corresponding authors: "Improving Parallel State-Space Exploration Using Genetic Algorithms" Etienne Renault (1) (1) LRDE, Epita, Paris, France Abstract: The verification of temporal properties against a given system may require the exploration of its full state space. In explicit model-checking this exploration uses a Depth-First-Search (DFS) and can be achieved with multiple randomized threads to increase performance. Nonetheless the topology of the state-space and the exploration order can cap the speedup up to a certain number of threads. This paper proposes a new technique that aims to tackle this limitation by generating artificial initial states, using genetic algorithms. Threads are then launched from these states and thus explore different parts of the state space. Our prototype implementation runs 10% faster than state-of-the-art algorithms. These results demonstrate that this novel approach worth to be considered as a way to overcome existing limitations. More information at : https://www.lrde.epita.fr/wiki/Publications/renault.18.vecos <https://www.lrde.epita.fr/wiki/Publications/renault.18.vecos>

6 years, 11 months

Accepted paper at SYNT 2018

by Colange Maximilien

Greetings, We are pleased to announce that the following article has been accepted for publication in the 7th Workshop on Synthesis (SYNT@CAV 2018), to be held in Oxford on July, 18th 2018. "Reactive Synthesis from LTL Specification with Spot" Thibaud Michaud (LRDE -- EPITA) Maximilien Colange (LRDE -- EPITA) Abstract: We present ltlsynt, a new tool for reactive synthesis from LTL specifications. It relies on the efficiency of Spot to translate the input LTL specification to a deterministic parity automaton. The latter yields a parity game, which we solve with Zielonka's recursive algorithm. The approach taken in ltlsynt was widely believed to be impractical, due to the double-exponential size of the parity game, and to the open status of the complexity of parity games resolution. ltlsynt ranked second of its track in the 2017 edition of the SYNTCOMP competition. This demonstrates the practical applicability of the parity game approach, when backed by efficient manipulations of omega-automata such as the ones provided by Spot. We present our approach and report on our experimental evaluation of ltlsynt to better understand its strengths and weaknesses. -- Maximilien Colange Assistant Professor LRDE -- EPITA (+33) 1 53 14 59 45

6 years, 11 months

[Seminaire-LRDE] Séminaire du LRDE le mercredi 13 juin 2018: Camille Kurtz (LIPADE, Université Paris Descartes)

by Guillaume Tochon

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 13 juin 2018 (11h--12h), Amphi 401. 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/2018-06-13 [4] http://www.lrde.epita.fr/wiki/Contact Au programme du Mercredi 13 juin 2018 : * 11h--12h: Hierarchical image representations: construction, evaluation and examples of use for image analysis -- Camille Kurtz (LIPADE, Université Paris Descartes) www.math-info.univ-paris5.fr/~ckurtz/ Hierarchical image representations have become increasingly popular in image processing and computer vision over the past decades. Indeed, they allow a modeling of image contents at different (and complementary) levels of scales, resolutions and semantics. Methods based on such image representations have been able to tackle various complex challenges such as multi-scale image segmentation, image filtering, object detection, recognition, and more recently image characterization and understanding. In this talk, we will focus on the binary partition tree (BPT), which is a well-known hierarchical data-structure, frequently involved in the design of image segmentation strategies. In a first part, we will focus on the construction of such trees by providing a generalization of the BPT construction framework to allow one to embed multiple features, which enables handling many metrics and/or many images. In a second part, we will discuss how it may be possible to evaluate the quality of such a structure and its ability to reconstruct regions of the image corresponding to segments of reference given by a user. Finally, we will see some examples of image analysis and recognition processes involving these hierarchical structures. The main thematic application is remote sensing and satellite image analysis. -- Camille Kurtz obtained the MSc and PhD from Université de Strasbourg, France, in 2009 and 2012. He was a post-doctoral fellow at Stanford University, CA, USA, between 2012 and 2013. He is now an Associate Professor at Université Paris Descartes, France. His scientific interests include image analysis, data mining, medical imaging and remote sensing. 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. -- Guillaume TOCHON Maître de conférences // Assistant Professor LRDE, EPITA 18, rue Pasteur 94270 Le Kremlin-Bicêtre _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

6 years, 12 months

[Seminaire-LRDE] Séminaire du LRDE le mercredi 30 mai 2018: Jan Strejcek, Masaryk University

by Guillaume Tochon

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 30 mai 2018 (11h--12h), Amphi IP11. 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/2018-05-30 [4] http://www.lrde.epita.fr/wiki/Contact Au programme du Mercredi 30 mai 2018 : * 11h--12h: Partial but Precise Loop Summarization and Its Applications -- Jan Strejcek, Masaryk University https://www.fi.muni.cz/~xstrejc/ We show a symbolic-execution-based algorithm computing the precise effect of a program cycle on program variables. For a program variable, the algorithm produces an expression representing the variable value after the number of cycle iterations specified by parameters of the expression. The algorithm is partial in the sense that it can fail to find such an expression for some program variables (for example, it fails in cases where the variable value depends on the order of paths in the cycle taken during iterations). We present two applications of this loop summarization procedure. The first is the construction of a nontrivial necessary condition on program input to reach a given program location. The second application is a loop bound detection algorithm, which produces tighter loop bounds than other approaches. -- Jan Strejcek is an associate professor at the Faculty of Informatics of Masaryk University located in Brno, Czech Republic. He received his PhD in Computer Science (2005) and Master degrees in Mathematics (2000) and Computer Science (2001) from the same university. His current research focuses on automata over infinite words, automatic program analysis, and SMT-solving of quantified bitvector formulae. 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. -- Guillaume TOCHON Maître de conférences // Assistant Professor LRDE, EPITA 18, rue Pasteur 94270 Le Kremlin-Bicêtre _______________________________________________ Seminaire mailing list Seminaire(a)lrde.epita.fr https://lists.lrde.epita.fr/listinfo/seminaire

7 years

Programme du séminaire MeFoSyLoMa du 18 mai 2018 au LRDE

by Alexandre Duret-Lutz

======================================================================== Séminaire MeFoSyLoMa http://www.mefosyloma.fr/ Méthodes Formelles pour les Systèmes Logiciels et Matériels vendredi 18 mai 2018, 14h-16h30 Adresse: Amphi IP 11 24 rue Pasteur, 94270 Le Kremlin-Bicêtre Métro Porte d'Italie Plans d'accès : https://www.google.com/maps?q=48.815378,2.363106 https://www.lrde.epita.fr/~adl/img/plan-ip11.png 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-15h00: Étienne Renault (LRDE/EPITA), "The quest for an efficient LTL model-checking" Abstract: Model checking is an automated verification technique that is used for establishing that a model of a system is correct with respect to some given specification. One of the most serious problems with model checking in practice is the so-called "state explosion problem", i.e the state-space of a system can be too large to be processed in a reasonable time and to be stored on the memory. This problem can be addressed using symbolic or explicit techniques. In this talk I will focus on the latter one by overviewing the recent advances in (1) emptiness checks and (2) partial-order reductions. 15h00-15h30: Mathias Ramparison (LIPN, Université Paris 13), "Timed automata with parametric updates" Abstract: Timed automata (TAs) represent a powerful formalism to model and verify systems where concurrency is intricated with hard timing constraints. However, they can seem limited when dealing with uncertain or unknown timing constants. Several parametric extensions were proposed in the literature, and the vast majority of them leads to the undecidability of the EF-emptiness problem: "is the set of valuations reaching a given location empty?" Here, we study an extension of TAs where clocks can be updated to a parameter. While the EF-emptiness problem is undecidable for rational-valued parameters, it becomes PSPACE-complete for integer-valued parameters. In addition, exact synthesis of the parameter valuations set can be achieved. We also extend these two results to the EF-universality ("are all valuations reaching a given location?"), AF-emptiness ("is the set of valuations such that a given location is unavoidable empty?") and AF-universality ("are all valuations such that a given location is unavoidable?") problems. 15h30-16h00: pause café 16h00-16h30: vie du groupe 15h30-16h00: pause café 16h00-16h30: vie du groupe ======================================================================== -- Alexandre Duret-Lutz

7 years, 1 month

[COP 2018] CFP: 10th Workshop on Context-Oriented Programming (COP'18)

by Didier Verna

Call for Papers *** COP 2018: 10th International Workshop on Context-Oriented Programming *** July 16th, 2018 Co-located with ECOOP/ISSTA 2018 in Amsterdam, Netherlands === Advanced Modularity for Run-time Composition === Contextual information is playing an ever-increasing role in our information-centric world. Current-day software systems need to adapt continuously to changing execution and usage contexts, even while they are running. Unfortunately, mainstream programming languages and development environments still do not support this level of dynamic adaptivity very well, leading developers to implement complex designs to anticipate various dimensions of variability. Context-Oriented Programming directly supports variability at the programming level, featuring dedicated programming abstractions enabling programmers to write software applications that adapt dynamically to a wide range of dynamic attributes. It enables run-time behaviour to be dispatched directly on any detected properties of the execution or user context. Since more than a decade, several researchers have been working on a variety of notions approaching that idea. Implementations ranging from first prototypes to mature platform extensions used in commercial deployments have illustrated how multidimensional dispatch can be supported effectively to achieve expressive run-time variation in behavior. Our series of International Workshops on Context-Oriented Programming (COP) at ECOOP since 2009 have shown to be well-received, each attracting around 30 participants. Also in 2018 we hope to advance this vibrant research domain at ECOOP in the beautiful and lively city of Amsterdam. === Topics === Topics of interest to the workshop include, but are not limited to: - Interesting application domains and scenarios for COP - Programming language abstractions for COP (e.g. dynamic scoping, roles, traits, prototype-based extensions) - Implementation techniques and mechanisms for COP (e.g. different kinds of dynamic, contextual, and multi-dimensional dispatch or pre-dispatch) - Implementation issues for COP such as optimization, VM support, JIT compilation etc. - Implemented use-cases, case studies, or prototypes of COP - Theoretical foundations for COP (e.g., semantics, type systems) - Configuration languages (e.g. feature description interpreters, transformational approaches) - Interaction between non-functional programming concerns and COP (e.g. security, persistence, concurrency, distribution) - Modularization approaches for COP (e.g. modules, aspects, features, layers, plugins) - Guidelines to apply COP (e.g. best practices, idioms, patterns) - Run-time support for COP (e.g. reflection, dynamic binding) - Tool support (e.g. design tools, IDEs, debuggers) - Support for COP at the modeling level - Beyond context-oriented behavior adaptation (e.g., UI adaptation, DB adaptation). === Submission guidelines === COP invites submissions of high-quality papers reporting original research, or describing innovative contributions to, or experience with context-oriented programming, its implementation, and application. Papers that depart significantly from established ideas and practices are particularly welcome. Submissions must not have been published previously and must not be under review for any other refereed event or publication. The program committee will evaluate each contributed paper based on its relevance, significance, clarity, and originality. Papers are to be submitted via EasyChair (https://easychair.org/conferences/?conf=cop2018). They must be written in English, provided as PDF documents, and follow the new ACM Master Article Template with the sigconf option (https://www.acm.org/publications/proceedings-template). They should not exceed 8 pages. Accepted papers will be published in the ACM Digital Library. === Important dates === Submission deadline: May 18th, 2018 (AoE) Notifications: June 8th, 2018 Final version: June 29th, 2018 === Program committee === Tomoyuki Aotani, Tokyo Institute of Technology, Japan Nicolás Cardozo, Universidad de los Andes, Colombia Coen De Roover, Vrije Universiteit Brussel, Belgium Elisa Gonzalez Boix, Vrije Universiteit Brussel, Belgium David H. Lorenz, Technion IIT, Israel Gorel Hedin, Lund University, Sweden Stefan Marr, University of Kent, UK Kim Mens, Université Catholique de Louvain, Belgium Stefan Ramson, Hasso Plattner Institute, Germany Guido Salvaneschi, TU Darmstadt, Germany Matthias Springer, Tokyo Institute of Technology, Japan Mario Südholt, IMT Atlantique, France Naoyasu Ubayashi, Kyushu University, Japan Didier Verna, EPITA / LRDE, France Harumi Watanabe, Tokai University, Japan Tijs van der Storm, CWI, Netherlands === Organizing committee === Robert Hirschfeld, HPI, Germany Atsushi Igarashi, Kyoto University, Japan Tetsuo Kamina, Ritsumeikan University, Japan Jens Lincke, Hasso Plattner Institute, Germany Hidehiko Masuhara, Tokyo Institute of Technology, Japan -- Resistance is futile. You will be jazzimilated. Jazz site: http://www.didierverna.com Other sites: http://www.didierverna.info

7 years, 1 month

New journal publication: Lisp, Jazz, Aikido

by Didier Verna

Hello, I'm happy to announce the upcoming publication of my essay entitled Lisp, Jazz, Aikido, to appear in Volume 2 Issue 3 of the Art, Science and Engineering of Programming journal, in April 2018. The abstract is given below. The relation between Science (what we can explain) and Art (what we can't) has long been acknowledged and while every science contains an artistic part, every art form also needs a bit of science. Among all scientific disciplines, programming holds a special place for two reasons. First, the artistic part is not only undeniable but also essential. Second, and much like in a purely artistic discipline, the act of programming is driven partly by the notion of aesthetics: the pleasure we have in creating beautiful things. Eventhough the importance of aesthetics in the act of programming is now unquestioned, not much has been written on the subject. The field called "psychology of programming" focuses on the cognitive aspects of the activity, with the goal of improving the productivity of the programmers. Very few programmers have written about their thought process while programming either, and even fewer on their concern for aesthetics, and the impact it has on their activity. I can see three reasons for this. First, it may be frightening to do so. Reflecting on our aesthetic sensitivities involves thinking about our own emotions, and not everyone is ready or willing to perform that kind of introspection. Second, this introspection needs to be very deep, as our aesthetic sensitivities are extremely personal. Third, this introspection also needs to be very broad, as our aesthetic sensitivities affect every part of our lives. The purpose of this essay is to shed some new light on the art of programming by answering questions such as what makes us like or dislike such or such language or paradigm, or why do we shape our programs the way we do, all of this from the angle of aesthetics. Starting from the assumption that aesthetics is an inherently transversal concern, it should be possible for every programmer to find the same aesthetic driving force in every creative activity they undertake, not just programming, and in doing so, get deeper insight on why and how they do things the way they do. On the other hand, because our aesthetic sensitivities are so personal, all we can really do is relate our own experiences and share it with others, in the hope that it will inspire them to do the same. It is certainly an important purpose of this essay. My personal life has been revolving around three major creative activities, of equal importance: programming in Lisp, playing Jazz music and practicing Aikido. But why so many of them, why so different ones, and why these specifically? By introspecting my personal aesthetic sensitivities, I eventually realized that my tastes in the scientific, artistic and physical domains are all motivated by the same driving forces, hence unifying Lisp, Jazz and Aikido as three expressions of a single essence, not so different after all. In doing so, I gained considerable insight on my own psychology of programming, perhaps common to most lispers, perhaps also common to other programming communities. But that is for the reader to decide... -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

7 years, 1 month

Chapter published in Handbook of Parallel Constraint Reasoning

by Renault Etienne

Greetings, We are pleased to announce that the following chapter has been published in Handbook of Parallel Constraint Reasoning (Springer). Please find the title and abstract below. Title and corresponding authors: "Parallel Model Checking Algorithms for Linear-Time Temporal Logic" Jiri Barnat (1), Vincent Bloemen (2), Alexandre Duret-Lutz (3), Alfons Laarman (4), Laure Petrucci(5), Jaco van de Pol (2), and Etienne Renault (3) (1) Masaryk University, Brno, Czech Republic (2) University of Twente, Enschede, The Netherlands (3) LRDE, Epita, Paris, France (4) Leiden University, Leiden, The Netherlands (5) LIPN, CNRS, Paris, France Abstract: Model checking is a fully automated, formal method for demonstrating absence of bugs in reactive systems. Herebugs are violations of properties in Linear-time Temporal Logic (LTL). A fundamental challenge to its application is the exponential explosion in the number of system states. The current chapter discusses the use of parallelism in order to overcome this challenge. We reiterate the textbook automata-theoretic approach, which reduces the model checking problem to the graph problem of finding cycles. We discuss several parallel algorithms that attack this problem in various ways, each with different characteristics: Depth-first search (DFS) based algorithms rely on heuristics for good parallelization, but exhibit a low complexity and good on-the-fly behavior. Breadth-first search (BFS) based approaches, on the other hand, offer good parallel scalability and support distributed parallelism. In addition, we present various simpler model checking tasks, which still solve a large and important subset of the LTL model checking problem, and show how these can be exploited to yield more efficient algorithms. In particular, we provide simplified DFS-based search algorithms and show that the BFS-based algorithms exhibit optimal runtimes in certain cases. More information at : https://www.lrde.epita.fr/wiki/Publications/barnat.18.hpcr <https://www.lrde.epita.fr/wiki/Publications/barnat.18.hpcr>

7 years, 1 month

[Final CfPart] ELS 2018, April 16-17, Marbella, Spain

by Didier Verna

ELS'18 - 11th European Lisp Symposium Centro Cultural Cortijo de Miraflores Marbella, Málaga Spain April 16-17 2018 In cooperation with: ACM SIGPLAN Sponsored by RavenPack, Brunner Software GmbH, Franz Inc., LispWorks Ltd., and EPITA http://www.european-lisp-symposium.org/ Recent news: - ELS 2018 is in cooperation with ACM SIGPLAN - Full program now available on the website - Still one week to register! 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. Keynote speakers: - Vsevolod Domkin -- Lisp in a Startup: the Good, the Bad, and the Ugly - R. Matthew Emerson -- This Old Lisp (a look at Clozure CL) Important dates: - 16-17 Apr 2018 Symposium Programme chair: David Cooper, Genworks Intl., USA Local chairs: Andrew Lawson, Ravenpack, Spain Programme committee: Andy Wingo, Igalia, Spain Christophe Rhodes, Goldsmiths University, UK Christopher Wellons Null Program USA Ernst van Waning, Infometrics.nl, Netherlands Irène Durand, LaBRI, Université de Bordeaux, France Julian Padget, University of Bath, UK Ludovic Courtès, Inria, France Michael Sperber, DeinProgramm, Germany Nicolas Neuss, FAU Erlangen-Nürnberg, Germany Olin Shivers Northeastern University USA Philipp Marek, Austria Robert Strandh, Université de Bordeaux, France Sacha Chua Living an Awesome Life Canada Scott McKay, Future Fuel, USA Search Keywords: #els2018, ELS 2018, ELS '18, European Lisp Symposium 2018, European Lisp Symposium '18, 10th ELS, 10th European Lisp Symposium, European Lisp Conference 2018, European Lisp Conference '18 -- Resistance is futile. You will be jazzimilated. Lisp, Jazz, Aïkido: http://www.didierverna.info

7 years, 1 month

Accepted paper at ELS 2018

by Jim Newton

Greetings, I am pleased to announce that our paper "Approaches in Typecase Optimization” has been accepted to the next European Lisp Symposium, April 16-17, Marbella, Spain. Please find the abstract below. If anyone would like to take a look at the paper, your comments are welcome. https://www.lrde.epita.fr/dload/papers/newton.18.els.pdf <https://www.lrde.epita.fr/dload/papers/newton.18.els.pdf> Abstract We contrast two approaches to optimizing the Common Lisp typecase macro expansion. The first approach is based on heuristics intended to estimate run time performance of certain type checks involving Common Lisp type specifiers. The technique may, depending on code size, exhaustively search the space of permutations of the type checks, intent on finding the optimal order. With the second technique, we represent a typecase form as a type specifier, encapsulating the side-effecting non-Boolean parts so as to appear compatible with the Common Lisp type algebra operators. The encapsulated expressions are specially handled so that the Common Lisp type algebra functions preserve them, and we can unwrap them after a process of Boolean reduction into efficient Common Lisp code, maintaining the appropriate side effects but eliminating unnecessary type checks. Both approaches allow us to identify unreachable code, test for exhaustiveness of the clauses and eliminate type checks which are calculated to be redundant.

7 years, 1 month

← Newer
1
...
9
10
11
12
13
14
15
...
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