Annonce

Download

annonce@lrde.epita.fr

May 2018

2 participants
2 discussions

[Seminaire-LRDE] Séminaire du LRDE le mercredi 30 mai 2018: Jan Strejcek, Masaryk University
by Guillaume Tochon 17 May '18

17 May '18

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

1 0

Programme du séminaire MeFoSyLoMa du 18 mai 2018 au LRDE
by Alexandre Duret-Lutz 02 May '18

02 May '18

======================================================================== 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

1 0