BEGIN:VCALENDAR
PRODID:-//Google Inc//Google Calendar 70.9054//EN
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Inria Team Parkas
X-WR-TIMEZONE:Europe/Paris
X-WR-CALDESC:Shared PARKAS calendar (Inria Paris)
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20260226T100000
DTEND;TZID=Europe/Paris:20260226T110000
DTSTAMP;TZID=Europe/Paris:20260226T100000
UID:2026-02-26_Siron+Correnson
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Loïc Correnson: Modular Extraction of Lustre Models from C Reac
 tive Programs
URL:http://parkas.di.ens.fr/seminars.html#2026-02-26_Siron+Correnson
DESCRIPTION:Synchronous-reactive programming is a well-adopted formalism
  for analyzing \nand designing critical real-time systems. Reasoning at 
 the model level \nabstracts away all the complexities of low-level imper
 ative programming such \nas memory interactions. Consequently, many tool
 s are available to formally \nanalyze and verify synchronous programs. F
 or example, GATeL can be used to \ngenerate test sequences, and Kind2 ca
 n be used to verify safety properties. \nNevertheless, many real industr
 ial real-time systems are still written in \nplain C code today, while r
 eacting to the environment with a main loop, \nmaking them conceptually 
 synchronous-reactive programs. In this talk, we \npresent a methodology 
 to extract a Lustre synchronous-reactive model from a \nC Program. This 
 approach is based on both symbolic analysis and abstract \ninterpretatio
 n techniques to extract an equation system from a cyclic C \nprogram and
  simplify it in order to generate Lustre code.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20251211T140000
DTEND;TZID=Europe/Paris:20251211T150000
DTSTAMP;TZID=Europe/Paris:20251211T140000
UID:2025-12-11_Perami
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Thibaut Pérami: ArchSem: Reusable rigorous semantics of relaxed
  architectures
URL:http://parkas.di.ens.fr/seminars.html#2025-12-11_Perami
DESCRIPTION:The specifications of mainstream processor architectures, su
 ch as Arm, x86, \nand RISC-V, underlie modern computing, as the targets 
 of compilers, \noperating systems, and hypervisors. However, despite ext
 ensive research and \ntooling for instruction-set architecture (ISA) and
  relaxed-memory semantics, \nrecently including systems features, there 
 still do not exist integrated \nmathematical models that suffice for fou
 ndational formal verification, of \nconcurrent architecture properties o
 r systems software. Previous \nproof-assistant work has had to substanti
 ally simplify the ISA semantics, \nthe concurrency model, or both. We pr
 esent ArchSem, an architecture-generic \nframework for architecture sema
 ntics, modularly combining ISA and \nconcurrency models along a tractabl
 e interface of instruction-semantics \neffects, that covers a range of s
 ystems aspects. To do so, one has to handle \nmany issues that were prev
 iously unclear, about the architectures \nthemselves, the interface, the
  proper definition of reusable models, and the \nRocq and Isabelle idiom
 s required to make it usable. We instantiate it to \nthe Arm-A and RISC-
 V instruction-set architectures and multiple concurrency \nmodels. We de
 monstrate usability for proof, despite the scale, by \nestablishing that
  the Arm architecture (in a particular configuration) \nprovides a prova
 ble virtual memory abstraction, with a combination of Rocq, \nIsabelle, 
 and paper proof. Other work, not presented here, provides further \nconf
 irmation of usability, proving soundness of an Arm program logic. This \
 nestablishes a basis for future proofs of architecture properties and sy
 stems \nsoftware, above production architecture specifications.\n\nThis 
 work is in collaboration with\nThomas Bauereiss,\nBrian Campbell,\n[Zong
 yuan Liu](https://cs.au.dk/~zyliu/),\nNils Lauermann,\n[Alasdair Armstro
 ng](http://alasdair.io),\nand [Peter Sewell](https://www.cl.cam.ac.uk/~p
 es20/).\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20251203T170000
DTEND;TZID=Europe/Paris:20251203T180000
DTSTAMP;TZID=Europe/Paris:20251203T170000
UID:2025-12-03_Hughes
LOCATION:salle Emmy Noether; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:John Hughes: Experiences with QuickCheck: Testing the Hard Stuff
  and Staying Sane
URL:http://parkas.di.ens.fr/seminars.html#2025-12-03_Hughes
DESCRIPTION:_Organised together with the\n[ENS Informatics Department se
 minar](https://www.di.ens.fr/seminars)._\n\nFor most software developers
 , testing their code is more of a chore than a \npleasure. In this talk,
  I'll show you how to make testing a joyous \nexperience—by turning it
  into programming! QuickCheck is a property-based \ntesting tool, origin
 ally developed for Haskell, and now emulated in \nvirtually every progra
 mming language, which tests code in randomly generated \ncases, against 
 formal properties written as programs. It is surprisingly \neffective! I
 'll demonstrate the ideas on some ‘obviously correct’ C code, \nand 
 then tell a few war stories of using QuickCheck in industry, including \
 ntracking down a race condition that had plagued Klarna (Swedish online 
 \npayments giant) for years.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20250919T140000
DTEND;TZID=Europe/Paris:20250919T150000
DTSTAMP;TZID=Europe/Paris:20250919T140000
UID:2025-09-19_Kiselyov
LOCATION:salle Emmy Noether; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Oleg Kiselyov: A Compositional Semantics of Assignment — or, L
 -values Demystified and Deprecated
URL:http://parkas.di.ens.fr/seminars.html#2025-09-19_Kiselyov
DESCRIPTION:_Organised together with the \n[SemAntique](https://team.inr
 ia.fr/antique/semantique/)_\n\nIn Fortran/Algol tradition, a mutable var
 iable is a variable that can be directly mutated as such by assignment, 
 increment, etc. In contrast, ML tradition uses variables of reference ty
 pes, bound to ‘boxed values’, or reference cells. These are ordinary
 , lambda-calculus variables that can be substituted for but not mutated.
  What is mutated is their value: the ‘box’. The two models seem equi
 valent and easily relatable. When we actually try to relate them — in 
 the context of implicitly heterogeneous metaprogramming: writing OCaml a
 s if it were C — we discover many subtleties, which make the problem n
 early intractable. One complication is that mutable variables are not fi
 rst-class, and a compositional mapping of reference-type variables to mu
 table variables is simply impossible.\n\nUpon systematic investigation w
 e discover a way to formally relate the two traditions. Practically, we 
 can write (or generate) first-order OCaml code using reference-type vari
 ables without restrictions, and straightforwardly map it to the efficien
 t and idiomatic C and be certain of its meaning, in C. We may hence writ
 e in (a subset of) OCaml as if it were C, using to the full extent the m
 odules, higher-order functions and other abstraction facilities of OCaml
  — and obtaining all the performance of C code, benefiting from vector
 ization, etc. of modern C compilers.\n\nIn the Fortran/Algol tradition, 
 the semantics of assignment such as `x = x + 1` is non-compositional, an
 d to understand it, L-values were introduced decades ago. L-values simpl
 ify assignment by taking all the complexity upon themselves. Our relatio
 n of two traditions showed L-values are not needed. What is complicated 
 about assignment is not its semantics but an unusual syntax (sugar).\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20250917T171500
DTEND;TZID=Europe/Paris:20250917T181500
DTSTAMP;TZID=Europe/Paris:20250917T171500
UID:2025-09-17_Kiselyov
LOCATION:salle Emmy Noether; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Oleg Kiselyov: Higher-Performance Stream Processing: Theory and 
 Implementation
URL:http://parkas.di.ens.fr/seminars.html#2025-09-17_Kiselyov
DESCRIPTION:_subtitle:_ Stateful Stream Fusion as Normalization-by-Evalu
 ation\n\nWe present both a stream compilation theory and its implementat
 ion as a portable stream processing library [strymonas](http://strymonas
 .github.io/) with a familiar declarative interface and very high perform
 ance, notably exceeding all competition and attaining the performance of
  hand-written imperative state machines. The library targets: Java Strea
 ms-like applications; digital signal processing including software-defin
 ed radio; many sorts of sensor processing such as nested aggregations, c
 ompression/decompression.\n\nThe library lets us assemble complex stream
  pipelines just by plugging in simple combinators such as map, filter, f
 lat-map, zip, take, map-accumulate and sliding windowing. Strymonas stre
 ams may be infinite, stateful, with the generally variable and staticall
 y unknown processing rate.\n\nStrymonas is a code generator with pluggab
 le backends (currently generating C, OCaml and Scala). The pipeline comb
 inators may be freely composed, and yet the resulting convoluted imperat
 ive code contains no traces of combinator abstractions: no closures, int
 ermediate objects or tuples. The high-performance is portable and static
 ally guaranteed.\n\nStrymonas has been developed in tandem with the equa
 tional theory of stateful streams. Our theoretical model represents all 
 desired pipelines and guarantees the existence of unique normal forms, w
 hich are mappable to (fused) state machines. Stream pipeline compilation
  and optimization are represented as normalization-by-evaluation, and ar
 e hence deterministic and terminating, with the guaranteed outcome. The 
 equational theory lets us state and prove the correctness of the complet
 e fusion optimization. Strymonas also implements a novel form of typed c
 losure conversion.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20250523T110000
DTEND;TZID=Europe/Paris:20250523T120000
DTSTAMP;TZID=Europe/Paris:20250523T110000
UID:2025-05-23_Potop-Butucaru
LOCATION:salle Bourbaki; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Dumitru Potop-Butucaru: Reactive Machine Learning by Example
URL:http://parkas.di.ens.fr/seminars.html#2025-05-23_Potop-Butucaru
DESCRIPTION:Machine Learning is emphatically dataflow (and therefore rea
 ctive) in form \nwhen new layers and networks are described in research 
 papers. Surprisingly, \npractical ML algorithm description and implement
 ation in frameworks such as \nJax and compilers such as MLIR is resolute
 ly control flow. This is largely \ndue to the fact that ML frameworks - 
 key enablers of the ML boom - are \nproducts of the HPC and PL communiti
 es.\n\nWhile ML algorithms were simple sequential models and the key act
 ivity was \nsupervised training on stored Big Data, there were little di
 fferences \nbetween dataflow and control flow specification styles. But 
 as the \ncomplexity of the applications increases and the focus shifts t
 owards \nreactive ML applications such as embedded ML or Reinforcement L
 earning, a \nnatively reactive/dataflow specification style could provid
 e important \nadvantages at both specification and implementation level.
 \n\nWe will explore this topic through examples in our new MLR language,
  \nintroducing both advantages and new challenges.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20250515T110000
DTEND;TZID=Europe/Paris:20250515T120000
DTSTAMP;TZID=Europe/Paris:20250515T110000
UID:2025-05-15_Bouillard
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Anne Bouillard: Guaranteed performance analysis of networks with
  bandwidth-sharing schedulers
URL:http://parkas.di.ens.fr/seminars.html#2025-05-15_Bouillard
DESCRIPTION:Deficit Round-Robin (DRR) is a scheduling algorithm that is 
 often used in \nreal-time systems or communication networks for scheduli
 ng tasks, or \npackets. This scheduling algorithm guarantees a share of 
 the bandwidth to \neach class of traffic, proportional to its assigned q
 uantum. This is an \nexample of bandwidth-sharing policy, as well as oth
 er Round-Robin policies \nlike Weighted Round Robin (WRR). Analyzing a b
 andwidth-sharing policy \nnetwork requires two steps. The first step is 
 a single-node analysis to \ncompute the service that is guaranteed to ea
 ch class of traffic. Recent work \nshow that knowing the characteristics
  of the cross-traffic can improve this \nguarantee. The second step is a
  per-class analysis. When all per-node \nguarantees have been computed, 
 one FIFO network per class can be \nconstructed, and delay bounds can be
  computed. In this talk, we will show \nhow these two steps are interdep
 endent, especially when the DRR network has \ncyclic dependencies, and p
 resent an iterative scheme that improves both the \nperformance bounds a
 nd stability region compared to the state of the art.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20250313T110000
DTEND;TZID=Europe/Paris:20250313T120000
DTSTAMP;TZID=Europe/Paris:20250313T110000
UID:2025-03-13_Girault
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Alain Girault: Exploring the memory / execution time tradeoff in
  dataflow graphs
URL:http://parkas.di.ens.fr/seminars.html#2025-03-13_Girault
DESCRIPTION:Many computing systems are constrained by a fixed amount of 
 available shared \nmemory. Modeling applications with task graphs makes 
 it possible to analyze \nand optimize their memory usage. The NP-complet
 e problem studied here is \nfinding a parallel schedule of a given task 
 graph that minimizes its memory \npeak.\n\nOur first contribution is a m
 ethod that finds memory-optimal sequential \nschedules for a dataflow ta
 sk graph. Our method relies on graph \ntransformation rules and has a po
 lynomial complexity. On a large class of \ngraphs, it is able to compres
 s the graph into a single node that contains a \nsequential schedule opt
 imal w.r.t. the memory peak. Our approach also \napplies to SDF graphs a
 fter converting them into task graphs. However, since \nthat conversion 
 may produce very large graphs, we also propose a new \nsuboptimal method
 , similar to Partial Expansion Graphs, to reduce the \nproblem size. We 
 evaluate our approach on classic benchmarks, on which we \nalways outper
 form the state-of-the-art.\n\nFrom this optimal sequential schedule, our
  second contribution is a dynamic \nparallel scheduling algorithm, which
  consists of a ready list scheduling \nthat we adapt to take into accoun
 t a given memory peak constraint. Even when \nthe memory peak is the min
 imal one, we always produce parallel schedules \nthat meets the constrai
 nt, and that enjoys very good speedups w.r.t. the \nsequential schedule.
  It can also be applied to less harsh memory \nconstraints, leading to m
 ore substantial speedups. We compare with \nalternative approaches on mu
 ltiple applications expressed as task graphs \n(scientific workflows, si
 gnal processing filters). When memory constraints \nare close to their m
 inimum, our approach always succeeds in finding a \nparallel schedule me
 eting the given constraints, whereas the other \napproaches mostly fail.
  When memory constraints are significantly higher, \nour results are com
 parable to others for speedup. Furthermore, our approach \nis faster and
  can deal with very large task graphs (up to 50,000 nodes) \nusing a nai
 ve Python implementation.\n\nBased on joint work with [Pascal Fradet](ht
 tps://pop-art.inrialpes.fr/people/fradet/Fradet_fr.html) and [Alexandre 
 Honorat](https://ahonorat.github.io/).\n\nReferences:\n\n* P. Fradet, A.
  Girault, A. Honorat.\n  [Sequential Scheduling of Dataflow Graphs for M
 emory Peak Minimization](https://pop-art.inrialpes.fr/~fradet/PDFs/LCTES
 23.pdf). \n  LCTES'23. Orlando, FL, USA. June 2023.\n\n* P. Fradet, A. G
 irault, A. Honorat.\n  [Graph Transformations for Memory Peak Minimizati
 on by Scheduling](https://inria.hal.science/hal-04688921/document),\n  A
 CM Trans. on Embedded Computing Systems, 2024.\n\n* P. Fradet, A. Giraul
 t, A. Honorat.\n  [Parallel scheduling of task graphs with minimal memor
 y requirements](https://inria.hal.science/hal-04879748v1).\n  IPDPS'25. 
 Milan, Italy. June 2025.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20241220T140000
DTEND;TZID=Europe/Paris:20241220T170000
DTSTAMP;TZID=Europe/Paris:20241220T140000
UID:2024-12-20_Jeanmaire
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Paul Jeanmaire: Une sémantique dénotationnelle pour un compila
 teur synchrone vérifié
URL:http://parkas.di.ens.fr/seminars.html#2024-12-20_Jeanmaire
DESCRIPTION:This PhD defense will be presented in French. The abstract i
 n English can be \nfound below.\n\n_Soutenance de thèse_\n\nLustre est 
 un langage synchrone de type flot de données. Sa structure\ntemporelle 
 discrète et son système d'horloges lui permettent de garantir un\ntemp
 s d'exécution et une consommation de mémoire bornés statiquement,\nfa
 vorisant ainsi son adoption dans le domaine de systèmes\ncritiques, not
 amment au sein de l'outil industriel Scade.\nVélus, développé à l'In
 ria, est un compilateur Lustre vérifié. En s'appuyant\nsur la définit
 ion d'une sémantique formelle pour chaque langage intermédiaire,\nil a
 pporte une preuve qu'un programme Lustre et sa traduction en Clight\n(la
 ngage pris en charge par CompCert) exhibent des comportements identiques
 .\n\nDans cette thèse, nous développons un nouveau modèle du noyau fl
 ot de données\ndu langage d'entrée,\nbasé sur une sémantique dénota
 tionnelle synchrone, et donnons les conditions\nexactes de son équivale
 nce avec le modèle relationnel existant dans Vélus.\nCette approche co
 nstructive permet d'obtenir une sémantique exécutable,\nrenforçant ai
 nsi le principal théorème de correction de la compilation.\nGrâce au 
 principe d'induction de Scott, propre à la sémantique\ndénotationnell
 e, nous menons des raisonnements très naturels sur la dynamique\ndes pr
 ogrammes, moyennant un traitement explicite des erreurs pouvant\nsurveni
 r à l'exécution. Enfin, nous explorons la possibilité de\ns'affranchi
 r des contraintes de synchronisation du langage en proposant\nune corres
 pondance formelle de notre modèle avec celui des réseaux de Kahn.\nNou
 s esquissons les principes de l'infrastructure nécessaire à un raisonn
 ement\nvérifié de bout en bout sur les programmes compilables.\n\nLes 
 membres du jury sont\n* [Sylvain Boulmé](http://www-verimag.imag.fr/~bo
 ulme/) (Rapporteur), Grenoble-INP\n* [Christine Paulin-Mohring](https://
 www.lri.fr/~paulin/) (Rapporteur), Université Paris-Saclay\n* [Michael 
 Mendler](https://www.uni-bamberg.de/gdi/team/michael-mendler/), Universi
 té de Bamberg\n* [César A. Muñoz](https://shemesh.larc.nasa.gov/peopl
 e/cam/), NASA\n* [Xavier Rival](https://www.di.ens.fr/~rival/), Inria\n*
  [Yannick Zakowski](https://perso.ens-lyon.fr/yannick.zakowski/), Inria\
 n* [Timothy Bourke](https://www.tbrk.org), (Directeur de thèse), Inria\
 n* [Marc Pouzet](https://www.di.ens.fr/~pouzet/), (Directeur de thèse),
  École normale supérieure\n\n_PhD thesis defense_\n\nLustre is a synch
 ronous dataflow language. Its discrete temporal structure\nand clocking 
 system guarantee statically bounded execution time and memory\nconsumpti
 on, favoring its adoption in mission-critical systems, notably\nwithin t
 he Scade industrial tool. Vélus, developed at Inria, is a verified\nLus
 tre compiler. Based on the definition of formal semantics for each\ninte
 rmediate language, it provides a proof that a Lustre program and its\ntr
 anslation into Clight (the language supported by CompCert) exhibit\niden
 tical behaviors.\n\nIn this thesis, we develop a new model of the input 
 language's dataflow\nkernel, based on synchronous denotational semantics
 , and give the exact\nconditions for its equivalence with the existing r
 elational model in\nVélus. This constructive approach results in an exe
 cutable semantics,\nreinforcing the main correctness theorem of the comp
 ilation. Thanks to\nScott's induction principle, specific to denotationa
 l semantics, we are able\nto conduct very natural reasoning on program d
 ynamics, but with explicit\ntreatment of errors that may occur at runtim
 e. Finally, we explore the\npossibility of freeing ourselves from langua
 ge synchronization constraints by\nproposing a formal correspondence bet
 ween our model and that of Kahn's\nnetworks. We outline the principles o
 f the infrastructure required for an\nend-to-end verified reasoning on c
 ompilable programs.\n\nThe members of the thesis committee are\n* [Sylva
 in Boulmé](http://www-verimag.imag.fr/~boulme/) (Rapporteur), Grenoble-
 INP\n* [Christine Paulin-Mohring](https://www.lri.fr/~paulin/) (Rapporte
 ur), Université Paris-Saclay\n* [Michael Mendler](https://www.uni-bambe
 rg.de/gdi/team/michael-mendler/), Université de Bamberg\n* [César A. M
 uñoz](https://shemesh.larc.nasa.gov/people/cam/), NASA\n* [Xavier Rival
 ](https://www.di.ens.fr/~rival/), Inria\n* [Yannick Zakowski](https://pe
 rso.ens-lyon.fr/yannick.zakowski/), Inria\n* [Timothy Bourke](https://ww
 w.tbrk.org), (Directeur de thèse), Inria\n* [Marc Pouzet](https://www.d
 i.ens.fr/~pouzet/), (Directeur de thèse), École normale supérieure\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20241219T153000
DTEND;TZID=Europe/Paris:20241219T163000
DTSTAMP;TZID=Europe/Paris:20241219T153000
UID:2024-12-19_Bonneau
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Benjamin Bonneau: Une représentation intermédiaire pour la com
 pilation de programmes vériﬁés
URL:http://parkas.di.ens.fr/seminars.html#2024-12-19_Bonneau
DESCRIPTION:Les compilateurs effectuent des transformations sur les prog
 rammes, \nnotamment pour optimiser la performance du code généré. Ils
  doivent \ncependant s'assurer de la correction des transformations, c'e
 st-à-dire que \ntous les comportements du programme cible soient des co
 mportements autorisés \npar le programme source. Certaines transformati
 ons ne sont correctes que \nsous certaines conditions sémantiques (vale
 urs prises par les variables, \naliasing...). Les compilateurs ont donc 
 besoin d'obtenir ces informations, \nen effectuant des analyses ou en en
 codant les propriétés utiles dans les \nreprésentations (par exemple 
 avec des Undefined Behaviors).\n\nDans une première partie, je décrira
 i une représentation intermédiaire \nvisant à permettre l'encodage de
  propriétés connues sur le programme source. \nJe m'intéresse en part
 iculier à la compilation de programmes vérifiés ou \ngénérés, sur 
 lesquels on connaît des informations précises. J'utilise deux \nidées
  pour encoder les informations. D'une part, un système de types \ndépe
 ndants permet l'expression de propriétés et explicite les conditions q
 ui \nles assurent. D'autre part la représentation utilise de multiples 
 fragments \nmémoires au lieu d'une unique mémoire globale. On transmet
  ainsi des \ninformations précises sur l'aliasing. J'ai formalisé au s
 ein de l'assistant \nde preuve Rocq une sémantique dénotationnelle pou
 r cette représentation.\n\nDans une seconde partie, je décrirai une pa
 sse de compilation vérifiée d'un \nfragment de la représentation Obc 
 de Vélus vers ma représentation.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20241025T163000
DTEND;TZID=Europe/Paris:20241025T173000
DTSTAMP;TZID=Europe/Paris:20241025T163000
UID:2024-10-25_Wang
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Edward Wang: Work-in-Progress: An SMT-Based, Correct-by-Construc
 tion Place-and-Route Framework
URL:http://parkas.di.ens.fr/seminars.html#2024-10-25_Wang
DESCRIPTION:Place-and-route (P&R) plays a key bottleneck in integrated c
 ircuit design, \nand existing approaches for P&R fall short in correctne
 ss and methodology. \nWe introduce an SMT-based approach which addresses
  these concerns and \nintroduces some new possibilities for improved co-
 optimization of designs. \nWe introduce the system design and problem en
 coding and show some \npreliminary results to address the key challenge 
 of scalability.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20240606T110000
DTEND;TZID=Europe/Paris:20240606T120000
DTSTAMP;TZID=Europe/Paris:20240606T110000
UID:2024-06-04_Prasad
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Sanjiva Prasad: Secure Information Flow Connections
URL:http://parkas.di.ens.fr/seminars.html#2024-06-04_Prasad
DESCRIPTION:_Joint work with: Chandrika Bhardwaj, Goldman Sachs India_\n
 \nDenning's (1976) lattice model provided secure information flow analys
 es \nwith an intuitive mathematical foundation: the lattice ordering det
 ermines \npermitted flows. We propose a connection-based extension of th
 is framework \nthat permits two autonomous organisations, each employing
  possibly quite \ndifferent security lattices, to exchange information w
 hile maintaining \nsecurity of information flow as well as their autonom
 y in formulating and \nmaintaining security policies. Our prescriptive f
 ramework is based on the \nrigorous mathematical framework of Lagois con
 nections proposed by Melton, \ntogether with a simple type system and op
 erational model for transferring \nobject data between the two domains. 
 The merit of this formulation is that \nit is simple, minimal, adaptable
  and intuitive. We show that our framework \nis semantically sound, by p
 roving that the connections proposed preserve \nstandard correctness not
 ions such as noninterference. We then illustrate via \nexamples how Lago
 is theory also provides a robust framework and methodology \nfor negotia
 ting and maintaining secure agreements on information flow \nbetween aut
 onomous organisations, even when either or both organisations \nchange t
 heir security lattices. Composition and decomposition properties \nindic
 ate support for a modular approach to secure flow frameworks in complex 
 \norganisations. Finally, a natural and conservative extension of the \n
 Decentralised Labels Model of naturally induces a Lagois connection betw
 een \nthe corresponding security label lattices, thus extending the secu
 rity \nguarantees ensured by the decentralised model to encompass bidire
 ctional \ninterorganisational flows.\n\n_Bio_: Sanjiva Prasad is a Profe
 ssor of Computer Science and Engineering \n(CSE) at IIT Delhi, and curre
 nt Head of the  School of Public Policy (SPP). \nEarlier he headed the 
 CSE Department and the Khosla School of Information \nTechnology (SIT). 
 His research interests include formal methods, \nspecifically concurrenc
 y, programming languages and their semantics, \nsecurity of information 
 flow, formal foundations of networks, and medical \napplications of comp
 uting.  He is currently Co-Editor-in-Chief of ACM Books.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20240315T140000
DTEND;TZID=Europe/Paris:20240315T150000
DTSTAMP;TZID=Europe/Paris:20240315T140000
UID:2024-03-15_Incer
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Inigo Incer: Towards Provably Safe and Secure Systems with Contr
 act-Based Design
URL:http://parkas.di.ens.fr/seminars.html#2024-03-15_Incer
DESCRIPTION:The task of system design is shared by all engineering disci
 plines, each \ncoming with its own techniques. In spite of their differe
 nces in tools, \nthere is large intersection in their conceptual approac
 h to design. In this \ntalk, we exploit this commonality to take an abst
 ract view of systems and \ntheir composition. We understand systems and 
 subsystems in terms of their \nassume-guarantee specifications, or contr
 acts.\n\nAssume-guarantee contracts are formal specifications that state
  (i) the \nassumptions that a design element makes on its environment an
 d (ii) the \nguarantees it delivers when the environment behaves accordi
 ng to the \ncontract's assumptions. Contracts come with a rich algebra t
 hat allows us to \ncarry out several design-relevant tasks: obtaining sy
 stem-level \nspecifications from component specifications, finding speci
 fications of \ncomponents that need to be added to a design in order to 
 meet an objective, \netc. We will introduce the algebra of contracts and
  discuss how the various \nalgebraic operations relate to system-design 
 tasks. We will discuss \nhypercontracts, an extension of assume-guarante
 e reasoning to support the \nformal analysis of key security and robustn
 ess properties. We will also \ndiscuss the application of this methodolo
 gy and Pacti, a software package \nthat supports system design using con
 tracts, in applications ranging from \nspace-mission design to synthetic
  biology.\n\n_Bio_: Inigo Incer is a postdoctoral researcher at Caltech 
 and UC Berkeley. \nHe obtained his PhD from UC Berkeley in 2022 under th
 e guidance of Alberto \nSangiovanni-Vincentelli. He is interested in all
  aspects of cyber-physical \nsystems, emphasizing formal methods and AI 
 that support their compositional \ndesign and analysis. Before pursuing 
 a PhD, Inigo was an IC designer in \nAustin. His work has been supported
  by the NSF/ASEE eFellows program and the \nUC Berkeley Chancellor's Fel
 lowship\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20240221T133000
DTEND;TZID=Europe/Paris:20240221T143000
DTSTAMP;TZID=Europe/Paris:20240221T133000
UID:2024-02-21_Schmidt
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Andreas Schmidt: Rust: Safe Beyond Memory
URL:http://parkas.di.ens.fr/seminars.html#2024-02-21_Schmidt
DESCRIPTION:Rust has established a reputation for providing both memory 
 and thread \nsafety. When it comes to dependable software, this is a for
 midable \nfoundation but often not sufficient. In particular, correctly 
 handling \nunavoidable (but manageable) error conditions and managing re
 sources (such \nas time) is essential. This talk sheds light on “stati
 cally extracting error \nflows” as well as “automatic and dependable
  resource management at run- and \ncompile-time”.\n\n[slides](https://
 netzdoktor.eu/inria-intro/parkas.html)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20240201T140000
DTEND;TZID=Europe/Paris:20240201T150000
DTSTAMP;TZID=Europe/Paris:20240201T140000
UID:2024-02-01_Stolze
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Claude Stolze: Composable Partial Multiparty Session Types
URL:http://parkas.di.ens.fr/seminars.html#2024-02-01_Stolze
DESCRIPTION:We introduce partial sessions and partial (multiparty) sessi
 on types, in \norder to deal with open systems, i.e., systems with missi
 ng components.\nPartial sessions can be composed, and the type of the re
 sulting system is \nderived from those of its components without knowing
  any suitable global \ntype nor the types of missing parts.\nWe apply th
 ese types to a process calculus, for which we prove subject \nreduction 
 and progress, so that well-typed systems never violate the \nprescribed 
 constraints.\nTherefore, partial session types support the development o
 f systems by \nincremental assembling of components.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20231208T133000
DTEND;TZID=Europe/Paris:20231208T163000
DTSTAMP;TZID=Europe/Paris:20231208T133000
UID:2023-12-08_Pauget
LOCATION:CONF IV/E244 (2nd floor); 24 rue Lhomond; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY: Baptiste Pauget : Spécification de la mémoire dans un langage
  synchrone flot de données doté de tableaux de taille statique
URL:http://parkas.di.ens.fr/seminars.html#2023-12-08_Pauget
DESCRIPTION:This PhD defense will be presented in French. The abstract i
 n English can be \nfound below.\n\n_Soutenance de thèse (en français)_
 \n\nScade est un langage de programmation synchrone utilisé depuis la f
 in des \nannées 1990 pour concevoir et implémenter des systèmes criti
 ques embarqués \ntels ceux que l'on trouve dans l'aviation. Cette criti
 cité requiert la \nformalisation (i) des programmes, afin de garantir q
 u'ils s'exécutent sans \nerreurs ou retards pendant une durée arbitrai
 re et (ii) des outils de \ndéveloppement, en particulier le compilateur
 , pour s'assurer de la \npréservation des propriétés des modèles lor
 s de la génération de code. Ces \nactivités reposent sur une descript
 ion flot de données des modèles, inspirée \ndes schémas-blocs, dont 
 la sémantique s'exprime par des fonctions de suites, \nainsi que d'une 
 compilation précisément documentée.\n\nScade descend de Lustre. La ve
 rsion 6 a introduit des évolutions majeures, \ndans les pas de Lucid sy
 nchrone, dont les automates hiérarchique et les \ntableaux. Pour ces de
 rniers, leur taille est connue et vérifiée statiquement \nafin d'assur
 er un temps d'exécution et une mémoire bornés. L'utilisation \ncroiss
 ante des tableaux de Scade pour des opérations intensives a révélé \
 nplusieurs axes d'amélioration: verbosité des modèles, manque de cont
 rôle de \nla compilation ou description peu commode de certains algorit
 hmes.\n\nDans cette thèse, ces trois aspects ont été étudiés à l'a
 ide d'un prototype \nde compilateur. (i) Nous avons développé un syst
 ème de types a la \nHindley-Milner spécifiant les tailles sous la form
 e de polynômes \nmultivariés. Cette proposition permet de vérifier et
  d'inférer la plupart \ndes tailles de manière modulaire. (ii) Nous av
 ons exploré une méthode de \ncompilation alternative, fondée sur un l
 angage déclaratif conscient de la \nmémoire. Il vise à concilier le s
 tyle flot de données avec une spécification \nprécise des emplacement
 s mémoire. La description modulaire des tailles en \nest un élément c
 lé. (iii) Enfin, nous proposons une construction d'itération \ninspir
 ée de Sisal qui complète les itérateurs actuels. En traitant les \nta
 bleaux comme des suites finies, elle donne accès aux constructions \ns
 équentielles de Scade (automates) lors d'itérations. De plus, elle per
 met \nde décrire de manière déclarative des implémentations efficace
 s \nd'algorithmes comme la décomposition de Cholesky. Cette compilation
  \ncontrôlable est un premier pas nécessaire pour la compilation vers 
 des GPUs.\n\nLes membres du jury sont\n* [Albert Cohen](https://research
 .google/people/106208/) (Rapporteur), Google\n* [François Pottier](http
 s://pauillac.inria.fr/~fpottier/) (Rapporteur), Inria\n* [Jean-Louis Gia
 vitto](https://www.ircam.fr/person/jean-louis-giavitto), IRCAM\n* [Yamin
 e Ait-Ameur](https://www.researchgate.net/profile/Yamine-Ait-Ameur), Tou
 louse INP\n* [Alain Girault](https://pop-art.inrialpes.fr/~girault/), In
 ria Grenoble\n* [Laure Gonnord](https://laure.gonnord.org/pro/), Grenobl
 e INP\n* [Jean-Louis Colaço](https://www.researchgate.net/profile/Jean-
 Louis-Colaco), (Directeur de thèse), Ansys\n* [Marc Pouzet](https://www
 .di.ens.fr/~pouzet/), (Directeur de thèse), École normale supérieure\
 n\n__Memory Specification in a Data-flow Synchronous Language with Stati
 cally Sized Arrays__\n\n_PhD thesis defense (in French)_\n\nThe synchron
 ous programming language Scade has been used since the end of \nthe 1990
 s to design safety critical embedded systems such as those found in \nav
 ionics. This context requires to formally reason about (i) the programs,
  \nto ensure that they run for an arbitrary long time without errors or 
 missed \ndeadlines and (ii) the tools, in particular the compiler, to gi
 ve high \nconfidence in the preservation of model properties through the
  code \ngeneration process. These activities build on a data-flow descri
 ption of \nmodels, inspired by block diagrams, that enjoys a formal sema
 ntics in terms \nof streams and a well-documented compilation process.\n
 \nScade stems from Lustre. The Scade 6 version introduced major evolutio
 ns \nfollowing Lucid synchrone, notably hierarchical automata and arrays
 . For the \nlatter, sizes are statically known and checked, so as to ful
 fill the bounded \nresources and execution time constraints. The increas
 ing use of Scade arrays \nfor data-intensive computations has revealed a
 reas for improve- ment: \nconcision of the models, control of the genera
 ted code and idiomatic \ndescription of array computations.\n\nUsing a p
 rototype implementation of a compiler, the present work \ninvestigates t
 hese three aspects. (i) We designed a Hindley-Milner-like type \nsystem 
 for representing sizes with multivariate polynomials. This proposal \nal
 lows to check and infer most sizes in a modular way. (ii) We explored an
  \nalternative compilation process based on a memory-aware declarative \
 nlanguage. It aims at reconciling the data-flow style with a precise \ns
 pecification of memory locations. The underlying memory model builds on 
 our \nmodular description of sizes. (iii) Last, we propose an iteration 
 construct \ninspired by Sisal that supplements the available iterators. 
 By viewing \narrays as finite streams, iteration can benefit from the se
 quential \nconstructs of Scade, e.g., automata. Moreover, it allows decl
 arative \ndescriptions of efficient algorithm implementations such as th
 e Cholesky \ndecomposition. This controllable compilation process is a m
 andatory step \ntoward code generation for GPUs.\n\nThe members of the t
 hesis commitee are\n* [Albert Cohen](https://research.google/people/1062
 08/) (Reporter), Google\n* [François Pottier](https://pauillac.inria.fr
 /~fpottier/) (Reporter), Inria\n* [Jean-Louis Giavitto](https://www.irca
 m.fr/person/jean-louis-giavitto), IRCAM\n* [Yamine Ait-Ameur](https://ww
 w.researchgate.net/profile/Yamine-Ait-Ameur), Toulouse INP\n* [Laure Gon
 nord](https://laure.gonnord.org/pro/), Grenoble INP\n* [Alain Girault](h
 ttps://pop-art.inrialpes.fr/~girault/), Inria Grenoble\n* [Jean-Louis Co
 laço](https://www.researchgate.net/profile/Jean-Louis-Colaco), (Supervi
 sor), Ansys\n* [Marc Pouzet](https://www.di.ens.fr/~pouzet/), (Superviso
 r), École normale supérieure\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20231206T140000
DTEND;TZID=Europe/Paris:20231206T150000
DTSTAMP;TZID=Europe/Paris:20231206T140000
UID:2023-12-06_Sylvestre
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Loïc Sylvestre: Une approche synchrone pour la programmation ha
 ut-niveau de FPGA
URL:http://parkas.di.ens.fr/seminars.html#2023-12-06_Sylvestre
DESCRIPTION:Les FPGA sont des circuits reprogrammables qui constituent u
 ne cible de \nchoix, à la fois pour l'accélération matérielle d'appl
 ications logicielles \net pour l'interaction avec un environnement exté
 rieur (capteurs, \nactionneurs).\n\nDans cet exposé, je présenterai un
  noyau de langage fonctionnel synchrone \npour la conception d'applicati
 ons réactives embarquées sur FPGA. Chaque \napplication écrite dans c
 e langage est une fonction « instantanée » \nmodélisant directemen
 t un circuit synchrone qui reçoit des entrées et \nproduit des sorties
  à chaque cycle d'horloge.\n\nJe proposerai ensuite une extension conse
 rvative de ce langage avec des \ntraits de programmation de haut niveau 
 (récursion terminale, parallélisme à \ngros grain, tableaux implémen
 tés en mémoire RAM, voire même des structures \nde données dynamique
 s). Cette extension facilite la programmation \nd'applications réactive
 s incorporant des calculs « longs » progressant, pas \nà pas, de fa
 çon synchrone.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20231013T133000
DTEND;TZID=Europe/Paris:20231013T163000
DTSTAMP;TZID=Europe/Paris:20231013T133000
UID:2023-10-13_Pesin
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Basile Pesin: Verified Compilation of a Synchronous Dataflow Lan
 guage with State Machines
URL:http://parkas.di.ens.fr/seminars.html#2023-10-13_Pesin
DESCRIPTION:_PhD thesis defense._\n\n_There will be a “pot-de-thèse
 ” downstairs in the Cour aux Ernests after the \ndefense._\n_Extra inf
 ormation can be found on the dedicated [web \npage](https://vertmo.org/t
 hesis/)._\n\nSafety-critical embedded systems are often specified using 
 block-diagram \nformalisms. SCADE Suite is a development environment for
  such systems which \nhas been used industrially in avionics, nuclear pl
 ants, automotive and other \nsafety-critical contexts for twenty years. 
 Its graphical formalism \ntranslates to a textual representation based o
 n the Lustre synchronous \ndataflow language, with extensions from later
  languages like Lucid \nSynchrone. In Lustre, a program is defined as a 
 set of equations that relate \ninputs and outputs of the program at each
  discrete time step. The language \nof expressions at right of equations
  includes arithmetic and logic \noperators, delay operators that access 
 the previous value of an expression, \nand sampling operators that allow
  some values to be calculated less often \nthan others.\n\nThe Vélus pr
 oject aims at formalizing a subset of the Scade 6 language in \nthe Coq 
 Proof Assistant. It proposes a specification of the dynamic \nsemantics 
 of the language as a relation between infinite streams of inputs \nand o
 utputs. It also includes a compiler that uses CompCert, a verified \ncom
 piler for C, as its back end to produce assembly code, and an end-to-end
  \nproof that compilation preserves the semantics of dataflow programs.\
 n\nIn this thesis, we extend Vélus to support control blocks present in
  Scade 6 \nand Lucid Synchrone, which includes a construction that contr
 ols the \nactivation of equations based on a condition (switch), a const
 ruction that \naccesses the previous value of a named variable (last), a
  construction that \nre-initializes delay operators (reset), and finally
 , hierarchical state \nmachines, which allow for the definition of compl
 ex modal behaviors. All of \nthese constructions may be arbitrarily nest
 ed in a program. We extend the \nexisting semantics of Vélus with a nov
 el specification for these constructs \nthat encodes their behavior usin
 g sampling. We propose a generic induction \nprinciple for well-formed p
 rograms, which is used to prove properties of the \nsemantic model such 
 as determinism and type system correctness. Finally, we \ndescribe the e
 xtension of the Vélus compiler to handle these new constructs. \nWe sho
 w that the existing compilation scheme that lowers these constructs \nin
 to the core dataflow language can be implemented, specified and verified
  \nin Coq. Compiling the reset and last constructs requires deeper chang
 es in \nthe intermediate languages of Vélus.\n\nThe members of the thes
 is committee are\n* [Magnus Myreen](https://www.cl.cam.ac.uk/~mom22/) (R
 eporter),\n  Chalmers\n* [Robert de Simone](http://www-sop.inria.fr/memb
 ers/Robert.De_Simone/) (Reporter),\n  Inria\n* Carlos Agon,\n  IRCAM\n* 
 [Julien Forget](https://pro.univ-lille.fr/julien-forget),\n  Université
  de Lille\n* [Xavier Leroy](https://xavierleroy.org/),\n  Collège de Fr
 ance\n* [Timothy Bourke](https://www.tbrk.org) (Supervisor),\n  Inria an
 d ENS\n* [Marc Pouzet](https://www.di.ens.fr/~pouzet/) (Supervisor),\n  
 ENS and Inria\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20231013T090000
DTEND;TZID=Europe/Paris:20231013T100000
DTSTAMP;TZID=Europe/Paris:20231013T090000
UID:2023-10-13_Myreen
LOCATION:salle Lions 1; bâtiment C; Inria Paris; 2 rue Simone Iff; Pari
 s 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Magnus Myreen: The CakeML Project: Verified Compilation, Verifie
 d Bootstrapping, Just-In-Time Compilation, and Applications
URL:http://parkas.di.ens.fr/seminars.html#2023-10-13_Myreen
DESCRIPTION:_Attention: This is a joint Parkas/Cambium seminar held at I
 nria Paris in \nthe 12e_\n\nThis talk will be about the [CakeML](https:/
 /cakeml.org/) project. The \nCakeML project centres around an impure fun
 ctional programming language, for \nwhich we have developed a collection
  of proofs and tools inside the \n[HOL4](https://hol-theorem-prover.org/
 ) theorem prover. The development \nincludes a proven-correct compiler t
 hat can bootstrap itself.\n\nThis talk has two parts.\n\nIn the first pa
 rt, I will explain the research questions the CakeML project \nhas tackl
 ed and outline the main research ideas that have helped us address \nthe
 m. The research questions include:\n\n- how can we transfer properties p
 roved of logic functions to\n  properties of machine code compiled from 
 those functions?\n- how can we use a verified compiler to compile itself
 ?\n- how can we reason about space usage of CakeML programs?\n- how can 
 we prove liveness properties for non-terminating code?\n\nIn the second 
 part, I will describe how the CakeML project strives to\nbuild meaningfu
 l connections with other projects and our experience\nwith this so far. 
 We have:\n\n- built a proved-to-be-sound clone of the HOL light theorem 
 prover\n- produced a verified compiler for a Haskell-like language\n- co
 nstructed several verified checkers, including checkers for UNSAT\n  pro
 ofs, floating-point error bounds, OpenTheory article files,\n  pseudo-Bo
 olean proofs, and Integer Programming proofs\n\nThe CakeML project is a 
 collaborative open source project and we are always \nkeen to explore ne
 w directions and collaborations.\n\nThe CakeML webpage: <https://cakeml.
 org/>\n\nThe CakeML project lives in the HOL4 theorem prover:\n<https://
 hol-theorem-prover.org/>\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20230718T153000
DTEND;TZID=Europe/Paris:20230718T163000
DTSTAMP;TZID=Europe/Paris:20230718T153000
UID:2023-07-18_Cohen
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Albert Cohen: Bidirectional Reactive Programming for Machine Lea
 rning
URL:http://parkas.di.ens.fr/seminars.html#2023-07-18_Cohen
DESCRIPTION:Reactive programming languages are dedicated to the programm
 ing of systems \nwhich react continuously with their environment. An env
 ironment is commonly \nassociated with physical sensors in a control sys
 tem, but it may also model \ninteractions with another program over time
 , or even the concurrency of the \nunderlying hardware platform. Values 
 take the form of unbounded streams, \nmodeling the (discrete) passing of
  time or the sequence of concurrent \ninteractions, and computations res
 ult from the implicit application of the \n`fold_left` iterator over poi
 ntwise reactions on streams. While `fold_left` \nimplements forward recu
 rrences, we introduce symmetric reactive semantics \ncorresponding to th
 e implicit application of the `fold_right` iterator, \nenabling what we 
 would like to refer to as bidirectional reactive \nprogramming. Constrai
 nts on backward recurrences allow to preserve important \nproperties of 
 reactive languages, including and bounded memory and reaction \ntime. Ma
 chine Learning (ML) systems provide numerous motivations for this: \nwe 
 demonstrate that reverse-mode automatic differentiation, backpropagation
 , \nbatch normalization, bidirectional recurrent neural networks, traini
 ng and \nreinforcement learning algorithms, are all naturally captured a
 s \nbidirectional reactive programs. We will discuss our ongoing progres
 s in the \narea.\n\n_(Joint work with Dumitru Potop-Butucaru and Hugo Po
 mpougnac.)_\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20230627T160000
DTEND;TZID=Europe/Paris:20230627T170000
DTSTAMP;TZID=Europe/Paris:20230627T160000
UID:2023-06-27_Guatto
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Adrien Guatto: Permissions, fonctions, récursion, normalisation
URL:http://parkas.di.ens.fr/seminars.html#2023-06-27_Guatto
DESCRIPTION:(En collaboration avec C. Tasson.)\n\nPlusieurs travaux réc
 ents et moins récents suggèrent d'intégrer une notion \nabstraite de 
 permission au cœur d'un langage de programmation. Les \npermissions doi
 vent a minima pouvoir être comparées et combinées, \nc'est-à-dire ap
 partenir à un préordre monoïdal.\n\nCet exposé traitera dans un prem
 ier temps d'un λ-calcul simplement typé où \nla gestion des permissio
 ns est présentée sous forme fonctionnelle, \nc'est-à-dire introduite 
 via une construction d'abstraction et éliminée via \nune construction 
 d'application. Le langage exhibe les propriétés attendues \ndes λ-cal
 culs typés (réduction du sujet, confluence, normalisation) et ce \nque
 l que soit le préordre monoïdal des permissions considéré.\n\nDans u
 n second temps, j'instancierai ce langage générique sur le préordre \
 nmonoïdal des horloges synchrones, et y ajouterai la récursion gardée
  et les \nsuites infinies. Je conjecture que les programmes bien typés 
 du langage \nobtenu sont productifs et synchrones : toute sortie d'une f
 onction de suites \ndéfinissable contient une infinité d'éléments do
 nt chacun ne dépend que des \néléments de rang inférieur des entrée
 s. Je discuterai enfin de la \npossibilité de formuler la productivité
  comme un résultat de normalisation \ninfinitaire.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20230621T143000
DTEND;TZID=Europe/Paris:20230621T153000
DTSTAMP;TZID=Europe/Paris:20230621T143000
UID:2023-06-21_Sankur
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Ocan Sankur: Model Checking Algorithms for Real-time Systems
URL:http://parkas.di.ens.fr/seminars.html#2023-06-21_Sankur
DESCRIPTION:Model checking is a technique for exhaustive verification. A
 lthough recent \nalgorithms allow one to verify large models, the scalab
 ility is still \nlimited for models with real-time constraints, that is,
  when time delays, \nexecution times, and deadlines are modeled explicit
 ly. In this talk, we \npresent some attempts to develop efficient algori
 thms for model checking \ntimed automata with large discrete state space
 s using techniques based on \npredicate abstraction, binary decision dia
 grams, SMT solvers, and automata \nlearning algorithms.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20230425T140000
DTEND;TZID=Europe/Paris:20230425T150000
DTSTAMP;TZID=Europe/Paris:20230425T140000
UID:2023-04-25_Broman
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:David Broman: Key aspects of the Miking framework: language comp
 osition, probabilistic domain-specific languages, and statically resolva
 ble ambiguity
URL:http://parkas.di.ens.fr/seminars.html#2023-04-25_Broman
DESCRIPTION:An essential benefit of domain-specific modeling languages i
 s that engineers and scientists can describe problems declaratively at a
  high level of abstraction. That is, users can focus on what to model ra
 ther than how to create an efficient implementation. Although there are 
 many benefits with well-engineered modeling languages, the development a
 nd maintenance cost can be very high. In this talk, I will give a brief 
 overview of a new framework called Miking that aims to address these cha
 llenges. Specifically, I will discuss some key aspects of the framework,
  including language fragments composition, DSLs for probabilistic progra
 mming, and a new concept called statically resolvable ambiguity.\n\n_Bi
 o:_\n\nDavid Broman is a Professor at the Department of Computer Science
 , KTH Royal Institute of Technology and an Associate Director Faculty fo
 r Digital Futures. He received his Ph.D. in Computer Science in 2010 fro
 m Linköping University, Sweden. Between 2012 and 2014, he was a visitin
 g scholar at the University of California, Berkeley, where he also was e
 mployed as a part-time researcher until 2016. His research focuses on th
 e intersection of (i) programming languages and compilers, (ii) real-tim
 e and cyber-physical systems, and (iii) probabilistic machine learning. 
 David has received a Distinguished Artifact Award at ESOP (co-authored 2
 022), an outstanding paper award at RTAS (co-authored 2018), a best pape
 r award in the journal Software & Systems Modeling (SoSyM award 2018), t
 he award as teacher of the year, selected by the student union at KTH (2
 017), the best paper award at IoTDI (co-authored 2017), and awarded the 
 Swedish Foundation for Strategic Research's individual grant for future 
 research leaders (2016). He has worked several years within the software
  industry, and is a member of IFIP WG 2.4, Modelica Association, a senio
 r member of IEEE, and a board member of Forskning och Framsteg.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20221124T090000
DTEND;TZID=Europe/Paris:20221124T100000
DTSTAMP;TZID=Europe/Paris:20221124T090000
UID:2022-11-24_Jeanin
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Jean-Baptiste Jeanin: Verification of Cyber-Physical Systems wit
 h Synchronous Programming, Refinement Types and Active Corners
URL:http://parkas.di.ens.fr/seminars.html#2022-11-24_Jeanin
DESCRIPTION:Robots and other cyber-physical systems are held to high sta
 ndards of safety \nand reliability. Formal verification can provide high
  assurance, but \nprogramming languages and techniques that lend themsel
 ves well to \nverification often do not produce executable code. We pres
 ent MARVeLus, a \nstream-based approach to combining verification and ex
 ecution in a \nsynchronous programming language with refinement types, b
 ased on Zélus. Our \napproach allows formal guarantees to be made about
  implementation-level \nsource code. We demonstrate the end-to-end proce
 ss of developing a safe \nrobotics application, from modeling and verifi
 cation to implementation and \nexecution.\n\nOne prominent example is th
 e verification of collision avoidance between \nvehicles. When we do not
  assume that the vehicles are point masses, the \nverification condition
 s can often not be discharged fully automatically. We \nconsider a conve
 x polygonal vehicle with nonzero area traveling along a \n2-dimensional 
 trajectory, and we derive an easily-checkable, quantifier-free \nformula
  to check whether a given obstacle will collide with the vehicle \nmovin
 g on the planned trajectory. Our technique compares favorably to \nquant
 ifier elimination in several case studies.\n\n_Bio:_\n\n[Jean-Baptiste J
 eannin](http://www-personal.umich.edu/~jeannin/) is an \nAssistant Profe
 ssor in [Aerospace Engineering](https://aero.engin.umich.edu) \nat the [
 University of Michigan](https://umich.edu), interested in Formal \nVerif
 ication and Programming Languages, and their applications to providing \
 nstrong guarantees to Aerospace, Robotics, and Cyber-Physical Systems. H
 e \nreceived an Engineering degree from École polytechnique, and a Ph.D
 . in \nComputer Science from Cornell University in 2013.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20221123T100000
DTEND;TZID=Europe/Paris:20221123T110000
DTSTAMP;TZID=Europe/Paris:20221123T100000
UID:2022-11-23_Pasteur
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Cédric Pasteur: Scade One, Embedded Software Design Reinvented
URL:http://parkas.di.ens.fr/seminars.html#2022-11-23_Pasteur
DESCRIPTION:In this presentation, I will introduce Scade One, the next g
 eneration of \nSCADE. I will present the high-level objectives and featu
 res of Scade One, \nwith demo videos of the Technology Preview.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20220520T160000
DTEND;TZID=Europe/Paris:20220520T170000
DTSTAMP;TZID=Europe/Paris:20220520T160000
UID:2022-05-20_Mendler
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Michael Mendler: Clocks Types for Synchronous Stream Processing 
 Revisited
URL:http://parkas.di.ens.fr/seminars.html#2022-05-20_Mendler
DESCRIPTION:Functional programming permits us to express complex computa
 tional \nabstractions very efficiently while using types to force these 
 abstractions \nto remain well-behaved. E.g., in second-order polymorphic
  lambda calculus \n(System F) we can define many standard inductive data
 -types so that \nwell-typed programs using these data types are guarante
 ed to be \ndeterministic and terminating.\n\nIt is natural to search for
  a “System F” for computational domains where not \nevery data type 
 is inductive. An important such domain is reactive data-flow \nprogrammi
 ng which is based on the co-inductive domain of polymorphic \nstreams. H
 ere, affairs turn a twist. While determinism is still important it \nis 
 the behavioural property of “progress” that we are concerned about: 
 A \nreactive computation must not terminate but instead exhibit an infin
 ite \nsequence of reaction cycles each of which should be finite (bounde
 d) in \nmemory and time. The type-free functional model of stream-proces
 sing by Kahn \nis very powerful but no "System K" is known that would un
 iformly guarantee \nprogress for Kahn-style stream-programming like Syst
 em F does for \nnon-interactive programming.\n\nHowever, interesting and
  practically useful type systems are known for \nspecial cases. This tal
 k revisits the type system proposed by Pouzet et al. \nfor the synchrono
 us programming languages Lucid Synchrone/Velus. It extends \nthe predica
 tive typing system of Hindley-Milner for data by “clock types” \nand
  “causality types” as additional layers to control synchronisation. 
 A \nwell-typed program is then guaranteed to be progressive, i.e., deadl
 ock-free \nand memory bounded, under a strictly synchronous model of sch
 eduling. For \npractical applications within the given restricted class 
 of synchronous \nprograms this achieves its goals. However, it remains o
 utside of a “System \nK” in the following sense: The typing system f
 irstly exploits dependent \ntypes and secondly it uses separate type sys
 tems, specifically, one for \neliminating deadlocks and another for elim
 inating unbounded memory. In the \ntalk we will discuss a variation to a
 void dependent types and to manage \ncausality and initialisation in one
  and the same typing language, without \n(hopefully) losing expressivene
 ss. The aim is to provide a more elementary \nreference calculus for tea
 ching purposes and a simpler basis for discussion \nof approximations of
  what might eventually become to be identified as \n“System K”.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20211122T090000
DTEND;TZID=Europe/Paris:20211122T183000
DTSTAMP;TZID=Europe/Paris:20211122T090000
UID:2021-11-22_Synchron
LOCATION:La Rochette; 35 minutes by train from Paris; Paris 5e
SEQUENCE:2
STATUS:CONFIRMED
SUMMARY: Workshop : Synchron 2021 — 28th International Open Workshop o
 n Synchronous Programming
URL:http://parkas.di.ens.fr/seminars.html#2021-11-22_Synchron
DESCRIPTION:The [PARKAS](https://parkas.di.ens.fr) team and Inria Paris 
 is organizing\n[Synchron 2021](http://synchron2021.inria.fr) over five d
 ays at the end of \nNovember.\n\nThe Open Synchron Workshop is the annua
 l meeting of experts and young \nresearchers in the area of synchronous 
 reactive programming. The main topics \ninclude executable specification
 s, program analysis, operational semantics, \nmodel-based design, formal
  methods, real-time programming, dedicated \narchitectures, timing predi
 ctability, and controller synthesis.\n\nThe genuine format of the Open S
 ynchron Workshop makes it unique in the \nmodern landscape: there is no 
 preliminary paper selection, and authors may \npresent their new work in
  any available slot on a first-come/first-served \nbasis. While the audi
 ence typically comprises a number of established \nresearchers in the to
 pic, newcomers are more than welcome. The cosy seminar \natmosphere crea
 ted by the venue in a single housing location is an \nopportunity for in
 formal discussions and exchanges between researchers of \ndiffering seni
 ority and expertise. Innovative contributions in blending \nreactive mod
 eling and programming notions with neighboring research subjects \nand c
 reative applicative domains, even at preliminary conceptual stages are \
 nalways greatly appreciated.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20201126T090000
DTEND;TZID=Europe/Paris:20201126T174500
DTSTAMP;TZID=Europe/Paris:20201126T090000
UID:2020-11-26_Synchron
LOCATION:online; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY: Online Workshop : Synchron 2020 — 27th International Open Wor
 kshop on Synchronous Programming
URL:http://parkas.di.ens.fr/seminars.html#2020-11-26_Synchron
DESCRIPTION:The [PARKAS](https://parkas.di.ens.fr) team is organizing\n[
 Synchron 2020](http://synchron2020.inria.fr) over two days at the end of
  \nNovember. Please join us online for 18 presentations from all over th
 e \nworld.\n\nThe Open Synchron Workshop is the annual meeting of expert
 s and young \nresearchers in the area of synchronous reactive programmin
 g. The main topics \ninclude executable specifications, program analysis
 , operational semantics, \nmodel-based design, formal methods, real-time
  programming, dedicated \narchitectures, timing predictability, and cont
 roller synthesis.\n\nThe genuine format of the Open Synchron Workshop ma
 kes it unique in the \nmodern landscape: there is no preliminary paper s
 election, and authors may \npresent their new work in any available slot
  on a first-come/first-served \nbasis. While the audience typically comp
 rises a number of established \nresearchers in the topic, newcomers are 
 more than welcome. The cosy seminar \natmosphere created by the venue in
  a single housing location is an \nopportunity for informal discussions 
 and exchanges between researchers of \ndiffering seniority and expertise
 . Innovative contributions in blending \nreactive modeling and programmi
 ng notions with neighboring research subjects \nand creative applicative
  domains, even at preliminary conceptual stages are \nalways greatly app
 reciated.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20200706T083000
DTEND;TZID=Europe/Paris:20200706T123000
DTSTAMP;TZID=Europe/Paris:20200706T083000
UID:2020-07-06_Brun
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Lélio Brun: Mechanized Semantics and Verified Compilation for a
  Dataflow Synchronous Language with Reset
URL:http://parkas.di.ens.fr/seminars.html#2020-07-06_Brun
DESCRIPTION:PhD thesis defense.\n\n_This will be an online thesis defens
 e. Please \n[connect](https://global.gotomeeting.com/join/281254693) wit
 h GoToMeeting \nusing your full name before the meeting is locked at 8:2
 0am.\nIt may be possible to join us physically at the ENS and there may 
 also be a \n“pot” in the Cours Pasteur after the defense.\nWe don't 
 know yet. Watch this space (or contact \n[Lélio](mailto:Lelio.Brun@inri
 a.fr))!_\n\nSpecifications based on block diagrams and state machines ar
 e used to design \ncontrol software, especially in the certified develop
 ment of safety-critical \napplications.\nTools like SCADE and Simulink/S
 tateflow are equipped with compilers that \ntranslate such specification
 s into executable code.\nThey provide programming languages for composin
 g functions over streams as \ntypified by dataflow synchronous languages
  like Lustre.\n\nIn this thesis we present Vélus, a Lustre compiler ver
 ified in the \ninteractive theorem prover Coq.\nWe develop semantic mode
 ls for the various languages in the compilation \nchain, and build on th
 e verified CompCert C compiler to generate executable \ncode and give an
  end-to-end correctness proof.\nThe main challenge is to show semantic p
 reservation between the dataflow \nparadigm and the imperative paradigm,
  and to reason about byte-level \nrepresentations of program states.\n\n
 We treat, in particular, the modular reset construct, a primitive for \n
 resetting subsystems.\nThis necessitates the design of suitable semantic
  models, compilation \nalgorithms and corresponding correctness proofs.\
 nWe introduce a novel intermediate language into the usual clock-directe
 d \nmodular compilation scheme of Lustre.\nThis permits the implementati
 on of compilation passes that generate better \nsequential code, and fac
 ilitates reasoning about the correctness of the \nsuccessive transformat
 ions of the modular reset construct.\n\nThe members of the thesis commit
 tee are\n* [Gerwin Klein](https://www.cse.unsw.edu.au/~kleing/) (Reporte
 r),\n  Data61/University of NSW\n* [Xavier Thirioux](http://thirioux.per
 so.enseeiht.fr/) (Reporter),\n  ISAE-SUPAERO\n* Jean-Louis Colaço,\n  A
 NSYS\n* Emmanuel Ledinot,\n  THALES Research &amp; Technology\n* [Xavier
  Leroy](https://xavierleroy.org/),\n  Collège de France\n* [Pascal Raym
 ond](http://www-verimag.imag.fr/~raymond/),\n  Université Grenoble-Alpe
 s, CNRS, and VERIMAG\n* [Timothy Bourke](https://www.tbrk.org) (Supervis
 or),\n  Inria and ENS\n* [Marc Pouzet](https://www.di.ens.fr/~pouzet/) (
 Supervisor),\n  Sorbonne Université, ENS, and Inria\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20200226T170000
DTEND;TZID=Europe/Paris:20200226T180000
DTSTAMP;TZID=Europe/Paris:20200226T170000
UID:2020-02-26_Lee
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Edward Lee: A Personal View of Real-Time Computing
URL:http://parkas.di.ens.fr/seminars.html#2020-02-26_Lee
DESCRIPTION:Computers are widely used in timing-sensitive applications s
 uch as \ncontrolling vehicles, factories, and medical devices. Today, re
 al-time \nbehavior of programs is a property that emerges from implement
 ations rather \nthan a property that is specified in models. Control ove
 r timing behavior of \nsoftware is difficult to achieve, and timing beha
 vior is neither predictable \nnor repeatable. I will argue that this pro
 blem can be solved by making a \ncommitment to deterministic models that
  embrace temporal properties as an \nintegral part of the modeling parad
 igm. I will explain how such models \ndiffer from the prevailing practic
 e of modeling low-level computer \narchitectures and estimating worst-ca
 se execution time. I will show moreover \nthat deterministic timing is p
 ractical today without sacrificing performance \nfor many useful workloa
 d models. Specifically, I will describe a class of \ncomputer architectu
 res called PRET Machines that deliver deterministic \ntiming with no los
 s of performance for a family of real-time problems \nconsisting of spor
 adic event streams with hard deadlines.\n\n_This talk is part of the [se
 minar series][1] of the Informatics Department \nat the ENS._\n\n[1]: ht
 tps://www.di.ens.fr/seminars\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20200221T110000
DTEND;TZID=Europe/Paris:20200221T120000
DTSTAMP;TZID=Europe/Paris:20200221T110000
UID:2020-02-21_Kiselyov
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Oleg Kiselyov: Even better stream fusion, as normalization-by-ev
 aluation
URL:http://parkas.di.ens.fr/seminars.html#2020-02-21_Kiselyov
DESCRIPTION:The [strymonas library (POPL 2017)][1] is a high-performance
  stream code \ngeneration library (DSL) that supports any combination of
  zipping, nesting \n(or flat-mapping), sub-ranging, filtering, mapping 
 — of finite or infinite \nstreams. Whatever the stream pipeline, strym
 onas delivers hand-written-like \ncode — but automatically, assuredly 
 and portably, with no reliance on \nblack-box optimizers or sufficiently
  smart compilers. Not only is the \nstrymonas-produced code free from in
 termediate data structures of unbounded \nsize, in many cases, the code 
 is free from any intermediate data structures \nwhatsoever; the main loo
 p can run without allocating any memory and without \nany use of GC.\n\n
 We report on the follow-up work, which clarifies the semantic model of \
 nstrymonas and views stream fusion as normalization-by-evaluation. As a 
 \nresult, we have reduced the number of core strymonas primitives and ma
 de \nthem more general. In the original strymonas, when zipping two stre
 ams both \ncontaining filtering or flat-mapping, fixed-size intermediate
  data \nstructures seemed inevitable. We have already demonstrated truly
  \nconstant-space zipping of filtered streams. Zipping of two flat-mappe
 d \nstreams is the only case that is still undecided (as of this writing
 ).\n\nThis is a joint work with Kobayashi Tomoaki.\n\n[1]: https://strym
 onas.github.io\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20190621T140000
DTEND;TZID=Europe/Paris:20190621T160000
DTSTAMP;TZID=Europe/Paris:20190621T140000
UID:2019-06-21_Reddy
LOCATION:CONF IV/E244 (2nd floor); 24 rue Lhomond; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Chandan Reddy: Polyhedral Compilation for Domain Specific Langua
 ges
URL:http://parkas.di.ens.fr/seminars.html#2019-06-21_Reddy
DESCRIPTION:PhD thesis defense.\n\nIn recent years the polyhedral model 
 has emerged as a powerful mathematical \nframework for loop transformati
 ons in optimizing compilers. In this thesis, \nwe study the applicabilit
 y of the polyhedral model to the compilation of \ndomain-specific langua
 ges, focusing on image processing and deep learning \npipelines. We prop
 ose new techniques to enhance the state-of-the-art \npolyhedral compilat
 ion toolchain to achieve peak performance close to highly \ntuned libari
 es. We extend a polyhedral toolchain to handle reductions which \nare a 
 key part of image processing and deep learning pipelines and often \nbec
 ome the bottleneck if not parallelized. We also extend the Pluto \nalgor
 ithm to account for the spatial locality in addition to the temporal \nl
 ocality. We also propose a schedule specialization method for given prob
 lem \nsizes.   Finally, we propose techniques to reduce the autotuning t
 ime from \nhours to minutes.\n\nThe members of the thesis committee are\
 n* [Cédric Bastoul](http://icps.u-strasbg.fr/people/bastoul/public_html
 /),\n  University of Strasbourg (Reporter)\n* [Saman Amarasinghe](https:
 //people.csail.mit.edu/saman/),\n  Massachusetts Institute of Technology
  (Reporter)\n* [Corinne Ancour](http://www.cri.ensmp.fr/people/ancourt/)
 ,\n  MINES ParisTech (Examiner)\n* [Christine Eisenbeis](http://pages.sa
 clay.inria.fr/christine.eisenbeis/)\n  INRIA Saclay (Examiner)\n* [Grigo
 ri Fursin](https://fursin.net/research.html),\n  Divitditi (Examiner)\n*
  [Albert Cohen](https://ai.google/research/people/106208),\n  Google and
  ENS (Supervisor)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20190610T150000
DTEND;TZID=Europe/Paris:20190610T170000
DTSTAMP;TZID=Europe/Paris:20190610T150000
UID:2019-06-10_Beaugnon
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Ulysse Beaugnon: Efficient Code Generation for Hardware Accelera
 tors by Refining Partially Specified Implementations
URL:http://parkas.di.ens.fr/seminars.html#2019-06-10_Beaugnon
DESCRIPTION:PhD thesis defense.\n\n_English_:\nCompilers looking for an 
 efficient implementation of a function must find \nwhich optimizations a
 re the most beneficial. This is a complex problem, \nespecially in the e
 arly steps of the compilation process. Each decision may \nimpact the tr
 ansformations available in subsequent steps. We propose to \nrepresent t
 he compilation process as the progressive refinement of a \npartially sp
 ecified implementation. All potential decisions are exposed \nupfront an
 d commute. This allows for making the most discriminative \ndecisions fi
 rst and for building a performance model aware of which \noptimizations 
 may be applied in subsequent steps. We apply this approach to \nthe gene
 ration of efficient GPU code for linear algebra and yield \nperformance 
 competitive with hand-tuned libraries.\n\n\n_Français_: Les compilateur
 s cherchant à améliorer l'efficacité des \nprogrammes doivent déterm
 iner quelles optimisations seront les plus \nbénéfiques. Ce problème 
 est complexe, surtout lors des premières étapes de \nla compilation o
 ù chaque décision influence les choix disponibles aux étapes \nsuivan
 tes. Nous proposons de représenter la compilation comme le raffinement 
 \nprogressif d’une implémentation partiellement spécifiée. Les déc
 isions \npossibles sont toutes connues dès le départ et commutent. Cel
 a permet de \nprendre les décisions les plus importantes en premier et 
 de construire un \nmodèle de performance capable d'anticiper les potent
 ielles optimisations. \nNous appliquons cette approche pour générer du
  code d'algèbre linéaire \nciblant des GPU et obtenons des performance
 s comparables aux bibliothèques \noptimisées à la main.\n\nThe member
 s of the thesis committee are:\n\n* [Francesco Zappa Nardelli](https://w
 ww.di.ens.fr/~zappa/),\n  (Examinateur and Président)\n* [Ratislav Bodi
 k](https://homes.cs.washington.edu/~bodik/),\n  University of Washington
  (Rapporteur)\n* [Christophe Dubach](http://homepages.inf.ed.ac.uk/cduba
 ch/),\n  University of Edinburgh (Rapporteur)\n* [Anton Lokhmotov](http
 s://uk.linkedin.com/in/lokhmotov),\n  [Dividity](https://www.dividiti.co
 m) (Examinateur)\n* [Jacques Pienaar](https://www.linkedin.com/in/jacque
 spienaar),\n  Google (Examinateur)\n* [Albert Cohen](https://ai.google/r
 esearch/people/106208),\n  [Google]() (Directeur de thèse)\n* [Marc Pou
 zet](https://www.di.ens.fr/~pouzet/),\n  ENS et Université Paris 6 (Cod
 irecteur de thèse)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20190515T150000
DTEND;TZID=Europe/Paris:20190515T160000
DTSTAMP;TZID=Europe/Paris:20190515T150000
UID:2019-05-15_Mercadier
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Darius Mercadier: Usuba: high-throughput & constant-time ciphers
 , by construction
URL:http://parkas.di.ens.fr/seminars.html#2019-05-15_Mercadier
DESCRIPTION:Cryptographic primitives are subject to diverging imperative
 s. The necessity \nof functional correctness and auditability pushes for
  using a high-level \nprogramming language. The performance requirements
  and the threat of timing \nattacks push for using no more abstract than
  an assembler to exploit (or \navoid!) the intricate micro-architectural
  features of a given machine. We \nbelieve that a suitable programming l
 anguage can reconcile both views and \nactually improve on the state of 
 the art in both directions. In this work, \nwe introduce Usuba, an opini
 onated dataflow programming language in which \nblock ciphers become so 
 simple as to be “obviously correct” and whose types \ndocument and e
 nforce valid parallelization strategies at the bit-level \ngranularity. 
 We then present Usubac, its optimizing compiler that produces \nhigh-thr
 oughput, constant-time implementations performing on par with \nhand-tun
 ed reference implementations. The cornerstone of our approach is a \nsys
 tematization and generalization of bitslicing, an implementation trick \
 nfrequently used by cryptographers. We thus show that Usuba can produce 
 code \nthat executes between 5% slower to 22% faster than hand-tuned ref
 erence \nimplementations while gracefully scaling across a wide range of
  \narchitectures and automatically exploiting Single Instruction Multipl
 e Data \n(SIMD) instructions whenever the cipher’s structure allows it
 .\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20190510T133000
DTEND;TZID=Europe/Paris:20190510T143000
DTSTAMP;TZID=Europe/Paris:20190510T133000
UID:2019-05-10_Forget
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Julien Forget: Data-dependencies in real-time multi-task program
 s
URL:http://parkas.di.ens.fr/seminars.html#2019-05-10_Forget
DESCRIPTION:A real-time system is a computer system that controls a phys
 ical device in \nits environment, at a rate adapted to the evolution of 
 the device. These \nsystems are often critical, as a malfunction can lea
 d to dramatic \nconsequences. Therefore, real-time system developers mus
 t ensure that their \nimplementations are safe, both functionally (produ
 cing the correct outputs) \nand temporally (producing outputs at the rig
 ht time).\n\nDeveloping a safe real-time system involves methods of two 
 rather\ndistinct research domains:\n\n1. formal methods, formal language
 s and compilation, for the functional \n   part;\n\n2. real-time schedul
 ing and Worst-Case Execution Time, for the temporal \n   part.\n\nThe ob
 jective of this talk is to focus on one specific area where both \ndomai
 ns meet, namely: *real-time data-dependencies*. A real-time system is \n
 typically programmed as a set of concurrent tasks, each with its own \nr
 eal-time constraints (periods, deadlines, ...). The talk will focus on t
 he \nsemantics, timing analysis, and implementation of inter-task \ndata
 -dependencies in such programs.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20190417T100000
DTEND;TZID=Europe/Paris:20190417T113000
DTSTAMP;TZID=Europe/Paris:20190417T100000
UID:2019-04-17_Todorov
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Vassil Todorov: Méthodes formelles au service de la voiture aut
 onome
URL:http://parkas.di.ens.fr/seminars.html#2019-04-17_Todorov
DESCRIPTION:La part croissante des fonctions d'assistance à la conduite
 , leur criticité, \nainsi que la perspective d'une certification de ces
  fonctions, rendent \nnécessaire leur vérification et leur validation 
 avec un niveau d'exigence \nque le test seul ne peut assurer. Depuis que
 lques années déjà d'autres \ndomaines comme l'aéronautique ou le fer
 roviaire sont soumis à des contextes \néquivalents. Pour répondre à 
 certaines contraintes ils ont localement mis en \nplace des méthodes fo
 rmelles. Le groupe PSA expérimente différentes \ntechniques formelles 
 afin de déterminer celles qui seraient pertinentes, \npour quel type de
  développement, ainsi que l'impact de leur déploiement sur \nle proces
 sus. Cette présentation fait un tour d'horizon des techniques \nformell
 es expérimentées sur du code embarqué réellement utilisé en \nprodu
 ction, donne une synthèse des résultats obtenus et propose quelques \n
 perspectives pour l'avenir.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20181213T100000
DTEND;TZID=Europe/Paris:20181213T123000
DTSTAMP;TZID=Europe/Paris:20181213T100000
UID:2018-12-13_Zhao
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Jie Zhao: A Combined Language and Polyhedral Approach for Hetero
 geneous Parallelism
URL:http://parkas.di.ens.fr/seminars.html#2018-12-13_Zhao
DESCRIPTION:PhD thesis defense. The room is on the very top floor, see [
 this \nmap](http://gdt.ludics.eu/index.php/Salle_W).\n\nThe work being p
 roposed concerns parallelization and optimizations for two \nimportant c
 lasses of applications: sparse computations and iterated \nstencils, tha
 t appear frequently in scientific simulation, learning \napplications, i
 mage processing, etc.\n\nNowadays, optimizing compilers are increasingly
  challenged by the diversity \nof programming languages and heterogeneit
 y of architectures.\nThe polyhedral model is a powerful mathematical fra
 mework for programs to \nexploit automatic parallelization and locality 
 optimization, playing an \nimportant role in the field of optimizing com
 pilers.\nA long standing limitation of the model has been its restrictio
 n to static \ncontrol affine programs, resulting in an emergent demand f
 or the support of \nnon-affine extensions.\nThis is particularly acute i
 n the context of heterogeneous architectures \nwhere a variety of comput
 ation kernels need to be analyzed and transformed \nto match the constra
 ints of hardware accelerators and to manage data \ntransfers across memo
 ry spaces.\nWe explore multiple non-affine extensions of the polyhedral 
 model, in the \ncontext of a well-defined intermediate language combinin
 g affine and \nsyntactic elements.\nOn the one hand, we explain how tran
 sformations and code generation for \nloops with non-affine, data-depend
 ent and dynamic loop bounds are integrated \ninto a polyhedral framework
 , extending the applicable domain of polyhedral \ncompilation in the rea
 lm of non-affine applications.\nOn the other hand, we describe the integ
 ration of overlapped tiling for \nstencil computations into a general po
 lyhedral framework, automating \nnon-affine transformations in polyhedra
 l compilation.\nWe evaluate our techniques on both CPU and CPU architect
 ures, validating the \neffectiveness of the optimizations by conducting 
 an in-depth performance \ncomparison with state-of-the-art frameworks an
 d manually-written libraries.\n\nThe members of the thesis committee ar
 e:\n\n* [Mary W. Hall](http://www.cs.utah.edu/~mhall/)\n  Professor, Uni
 versity of Utah (Reviewer)\n* [Cédric Bastoul](http://icps.u-strasbg.fr
 /people/bastoul/public_html/),\n  Professor, Université de Strasbourg (
 Reviewer)\n* Bill McColl, CTO/Fellow, Huawei Research/University of Oxfo
 rd (Examiner)\n* [Francesco Zappa Nardelli](https://www.di.ens.fr/~zappa
 /),\n  Senior Researcher, ENS Paris/INRIA (Examiner)\n* [Claude Tadonki]
 (https://www.cri.ensmp.fr/~tadonki/),\n  Senior Researcher, Mines ParisT
 ech/CRI (Examiner)\n* [Albert Cohen](https://who.rocq.inria.fr/Albert.Co
 hen/),\n  Research Scientist, Google (Advisor)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20181115T103000
DTEND;TZID=Europe/Paris:20181115T113000
DTSTAMP;TZID=Europe/Paris:20181115T103000
UID:2018-11-15_Abadi
LOCATION:Inria Paris; Salle Kions 1; bâtiment C; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Martín Abadi: On the Theory and Practice of Software that Learn
 s
URL:http://parkas.di.ens.fr/seminars.html#2018-11-15_Abadi
DESCRIPTION:*This is joint Parkas/Gallium seminar to be held at the Inri
 a Paris offices*\n\nAs machine learning becomes more powerful and pervas
 ive, it has an impact on\nthe many software systems that rely on it and 
 on the underlying software and\nhardware platforms. The resulting questi
 ons should concern virtually all\naspects of the theory and practice of 
 software, as they relate to software\nengineering, security and trust, p
 rogramming, tools, foundations, and\nmore. This talk will discuss some o
 f those questions. In particular, it will\npresent recent research on th
 e semantics of programming languages suitable for\nlearning by gradient 
 descent and on adversarial machine learning.\n\n_(This talk is a lightly
  updated version of one given at ETAPS 2018.)_\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20180926T140000
DTEND;TZID=Europe/Paris:20180926T150000
DTSTAMP;TZID=Europe/Paris:20180926T140000
UID:2018-09-26_Nobre
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Nuno Miguel Nobre: Polyhedral compilation of dataflow programs
URL:http://parkas.di.ens.fr/seminars.html#2018-09-26_Nobre
DESCRIPTION:Polyhedral techniques are an effective instrument in automat
 ic loop tiling \nfor data locality optimisation of sequential programs. 
 In this presentation, \nI will provide an example of how these technique
 s can be applied to \nautomatically adjust the granularity of work in a 
 one-dimensional \nGauss-Seidel kernel implemented in \n[OpenStream](htt
 p://openstream.cs.manchester.ac.uk/), a task-parallel \ndataflow languag
 e. Next, I will extend these ideas to the more \nrepresentative two-dime
 nsional case and compare the performance of these \npolyhedral-tiled Ope
 nStream programs against other implementations, e.g., a \nsequential C i
 mplementation, a parallel C implementation using OpenMP, and \nan implem
 entation using less convoluted OpenStream routines. Preliminary \nresult
 s show that our polyhedral-tiled versions are significantly faster \ntha
 n manually tiled OpenStream implementations, and thus demonstrate the \n
 value of polyhedral tiling for dataflow programming models. Given enough
  \nparallelism, our implementations also outperform polyhedral-tiled Ope
 nMP \nimplementations, suggesting that both polyhedral optimisations and
  the use \nof a task-parallel dataflow model contribute to better perfor
 mance.\n\n_Bio_: Nuno Migeul Nobre is currently a postgraduate research 
 student in the \nSchool of Computer Science at the University of Manches
 ter, UK, where he is \nstudying for a Ph.D. His research interests are f
 ocused on scheduling for \nheterogeneous multi-core architectures, langu
 ages and compilers for parallel \ncomputing and numerical algorithms.  H
 e also holds a master's degree in \nPhysics Engineering, awarded in 2016
  by the University of Coimbra, Portugal.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20180903T103000
DTEND;TZID=Europe/Paris:20180903T113000
DTSTAMP;TZID=Europe/Paris:20180903T103000
UID:2018-09-03_Hall
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Mary Hall: Bringing Sparse Computations into the Optimization Li
 ght
URL:http://parkas.di.ens.fr/seminars.html#2018-09-03_Hall
DESCRIPTION:Scalable computations where the data is sparse — that is, 
 a tiny subset\nof the data is populated — are widely represented in sc
 ientific\ncomputing and big data analytics.  Sparse data are typically r
 epresented\nby sparse matrices and graphs, which reduce data storage and
  computation\nrequirements (e.g., by storing only nonzero data elements)
  through the\nuse of indirection matrices such as `B` in `A[B[i]]`.  Thi
 s indirection\nimpacts performance on modern architectures.  Whether the
  code is\noptimized by human programmer, compiler or hardware, any optim
 izations\nthat must understand the memory access patterns for A require 
 the values\nof B, which are not known until runtime.  Over time, many op
 timizations\nof sparse computations have been developed that simplify th
 e code and\nreduce the amount of indirection through custom data represe
 ntations,\nbut these representations must also rely on runtime knowledge
  of the\nnonzero structure of the sparse data.  In this talk, we describ
 e a\nframework for composing compile-time and runtime optimizations of s
 parse\ncodes, and demonstrate its effectiveness at achieving performance
 \ncomparable to manually-tuned code for applications in scientific\ncomp
 uting and data analytics.\n\n_Bio_: Mary Hall is a professor in the Scho
 ol of Computing at University of\nUtah. She received a PhD in Computer S
 cience from Rice University.  Her\nresearch focus brings together compil
 er optimizations targeting current\nand future high-performance architec
 tures on real-world applications.\nHall's prior work has developed compi
 ler techniques for exploiting\nparallelism and locality on a diversity o
 f architectures: automatic\nparallelization for SMPs, superword-level pa
 rallelism for multimedia\nextensions, processing-in-memory architectures
 , FPGAs and more recently\nmany-core CPUs and GPUs. Professor Hall is an
  ACM Distinguished\nScientist and ACM’s representative on the Computin
 g Research Association\nBoard of Directors. She is deeply interested in 
 computing history,\nhaving served on the ACM History Committee for a dec
 ade and as chair\nfrom 2009-2014. She also actively participates in outr
 each programs to\nencourage the participation of women and underrepresen
 ted minorities in\ncomputer science.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20180413T110000
DTEND;TZID=Europe/Paris:20180413T120000
DTSTAMP;TZID=Europe/Paris:20180413T110000
UID:2018-04-10_Champion
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Adrien Champion: ICE-based Refinement Type Discovery for Higher-
 Order Functional Programs
URL:http://parkas.di.ens.fr/seminars.html#2018-04-10_Champion
DESCRIPTION:We propose a method for automatically finding refinement typ
 es of \nhigher-order function programs. Our method is an extension of th
 e ICE \nframework of Garg et al. for finding invariants. In addition to 
 the usual \npositive and negative samples in machine learning, their ICE
  framework uses \nimplication constraints, which consist of pairs (x, y)
  such that if x \nsatisfies an invariant, so does y. From these constrai
 nts, ICE infers \ninductive invariants effectively. We observe that the 
 implication \nconstraints in the original ICE framework are not suitable
  for finding \ninvariants of recursive functions with multiple function 
 calls. We thus \ngeneralize the implication constraints to those of the 
 form\n({x1,...,xk}, y), which means that if all of x1, ... , xk satis
 fy an \ninvariant, so does y. We extend their algorithms for inferring l
 ikely \ninvariants from samples, verifying the inferred invariants, and 
 generating \nnew samples. We have implemented our method and confirmed i
 ts effectiveness \nthrough experiments.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20180322T110000
DTEND;TZID=Europe/Paris:20180322T120000
DTSTAMP;TZID=Europe/Paris:20180322T110000
UID:2018-03-22_Brisk
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Philip Brisk: Language and Compiler Design for Laboratories-on-a
 -Chip
URL:http://parkas.di.ens.fr/seminars.html#2018-03-22_Brisk
DESCRIPTION:Microfluidics is a multidisciplinary field at the intersecti
 on of \nengineering, physics, chemistry, biochemistry, nanotechnology, a
 nd \nbiotechnology. It has practical applications to the design of integ
 rated \nsystems that process sub-microliter-scale volumes of fluid. Micr
 ofluidics \nhas enabled the emergence of a Laboratories-on-a-Chip (LoCs)
 , which \nintegrate multiple laboratory functions into devices whose phy
 sical size \nranges from square millimeters to square centimeters. Compa
 red to \ntraditional benchtop chemistry methods, LoCs offer the benefits
  of \nautomation and miniaturization; software-programmable LoCs offer a
 n \nimportant additional benefit: programmability.\n\nThis talk will int
 roduce BioScript, a domain-specific language for \nprogrammable LoCs, an
 d its compiler. Extensibility is particularly important \nfor language d
 esign, as each LoC target features a unique set of \ncapabilities, and t
 here is no universal functionality among LoCs akin to \nTuring completen
 ess. The BioScript compiler presently targets a specific \nclass of semi
 conductor-based LoCs which manipulate discrete liquid droplets \non a 2D
  electrode grid. The language, compiler, and runtime leverage \nadvances
  in sensor integration to execute biochemical procedures that \nfeature 
 online decision-making based on sensory data acquired during assay \nexe
 cution. The compiler features a novel hybrid intermediate representation
  \n(IR) that interleaves fluidic operations with computations performed 
 on \nsensor data. The IR extends the traditional notions of liveness and
  \ninterference to fluidic variables and operations, as needed to target
  the \nLoC, which itself can be viewed as a spatially reconfigurable arr
 ay. The \ncode generator converts the IR into the following:\n\n  1. a s
 et of electrode activation sequences for each basic block in the \n  con
 trol flow graph (CFG);\n  2. a set of computations performed on sensor d
 ata, which dynamically \n     determine the result of each control flow 
 operation; and\n  3. a set of electrode activation sequences for each co
 ntrol flow transfer \n  operation (CFG edge).\n\nThe compiler is validat
 ed using a software simulator which produces animated \nvideos of realis
 tic bioassay execution on the device. \n\n_Bio_: Philip Brisk received, 
 the BS, MS, and PhD Degrees, all in Computer \nScience, from UCLA in 200
 2, 2003, an 2006 respectively. From 2006-2009 he \nwas a Postdoctoral Sc
 holar at EPFL in Switzerland. He has been with UC \nRiverside since 2009
 . His research interests include programmable \nmicrofluidics and lab-on
 -a-chip technology, FPGAs and reconfigurable \ncomputing, and other forw
 ard-looking applications of computer engineering \nprinciples.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20171025T170000
DTEND;TZID=Europe/Paris:20171025T180000
DTSTAMP;TZID=Europe/Paris:20171025T170000
UID:2017-10-25_Mandel
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Louis Mandel: Prototyping a Query Compiler using Coq
URL:http://parkas.di.ens.fr/seminars.html#2017-10-25_Mandel
DESCRIPTION:Designing and prototyping new features is important in indus
 trial\nprojects. I will present our experience using the Coq proof assis
 tant\nas a prototyping environment for building a query compiler for use
  in\nIBM's ODM Insights. I will discuss the pros and cons of using Coq f
 or\nthis purpose and describe our methodology for porting the compiler t
 o\nJava for product integration.\n\nThe initial Coq prototype has evolve
 d into [Q*cert][1], an open-source \nplatform for the specification, ver
 ification, and implementation of query \ncompilers. This platform includ
 es support for SQL and OQL. It can generate \ncode for execution on Java
 Script, Spark and Cloudant. It internally relies \non familiar database 
 intermediate representations, notably the nested \nrelational algebra an
 d calculus. The platform also comes with a simple but \nfunctional and e
 xtensible query optimizers.\n\nThis is joint work with Joshua Auerbach, 
 Martin Hirzel, Avi Shinnar and \nJérôme Siméon.\n\n_This talk is [par
 t][2] of the seminar series of the Informatics Department \nat the ENS._
 \n\n[1]: https://querycert.github.io/\n[2]: http://www.di.ens.fr/Seminai
 reGeneral.html.fr#Mercredi_25_octobre_2017_17h00_L\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170928T103000
DTEND;TZID=Europe/Paris:20170928T113000
DTSTAMP;TZID=Europe/Paris:20170928T103000
UID:2017-09-28_DeBacker
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Bruno De Backer: EXEgesis: Understanding CPUs to speed up code
URL:http://parkas.di.ens.fr/seminars.html#2017-09-28_DeBacker
DESCRIPTION:Google's [EXEgesis project][1] takes a principled approach t
 o generating \ncode for modern processors. This talk will start with a r
 efresher on modern \ncomputer architectures. We shall see why it is impo
 rtant to have precise \ninstruction itineraries. We will then turn to th
 e combinatorial optimization \nmodels for obtaining these itineraries. W
 e will then touch on some gains \nthat we've obtained so far.\n\nThe EXE
 gesis team is based in the Google Paris office. Many of us have a \nback
 ground in combinatorial optimization, and we are passionate about CPUs.\
 n\n(NB: The [salle W][2] is well hidden. Please don't hesitate to come t
 o the \n[PARKAS][3] area beforehand. We will leave together at 10:20.)\n
 \n[1]: https://opensource.google.com/projects/exegesis\n[2]: http://gdt.
 ludics.eu/index.php/Salle_W\n[3]: http://parkas.di.ens.fr/#where
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170608T110000
DTEND;TZID=Europe/Paris:20170608T120000
DTSTAMP;TZID=Europe/Paris:20170608T110000
UID:2017-06-08_Nicolet
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Victor Nicolet: Synthesis of Divide And Conquer Parallelism for 
 Loops
URL:http://parkas.di.ens.fr/seminars.html#2017-06-08_Nicolet
DESCRIPTION:We focus on the automated synthesis of divide-and-conquer pa
 rallelism,\nwhich is a common parallel programming skeleton supported by
  many\ncross-platform multithreaded libraries. The challenges of produci
 ng\n(manually or automatically) a correct divide-and-conquer parallel pr
 ogram\nfrom a given sequential code are two-fold:\n\n1. assuming that in
 dividual worker threads execute a code identical to the \n   sequential 
 code, the programmer has to provide the extra code for \n   dividing the
  tasks and combining the computation results, and\n\n2. sometimes, the s
 equential code may not be usable as is, and may need to \n   be modified
  by the programmer.\n\nWe address both challenges in this paper. We pres
 ent an automated synthesis\ntechnique for the case where no modification
 s to the sequential code are\nrequired, and we propose an algorithm for 
 modifying the sequential code to\nmake it suitable for parallelization w
 hen some modification is necessary.\nFinally, we present theoretical res
 ults for when this modification is\nefficiently possible, and experiment
 al evaluation of the technique and the\nquality of the produced parallel
  programs.\n\n(This work will appear in [PLDI 2017](http://pldi17.sigpla
 n.org/event/pldi-2017-papers-automated-synthesis-of-divide-and-conquer-p
 arallelism).)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170405T140000
DTEND;TZID=Europe/Paris:20170405T170000
DTSTAMP;TZID=Europe/Paris:20170405T140000
UID:2017-04-05_Morisset
LOCATION:salle 236; 29 rue d'Ulm; ENS; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Robin Morisset: Compiler Optimisations and Relaxed Memory Consis
 tency Models
URL:http://parkas.di.ens.fr/seminars.html#2017-04-05_Morisset
DESCRIPTION:PhD thesis defense.\n\nThere will be a “pot-de-thèse” a
 fter the defense at 45 rue d'Ulm. Please \nRSVP to Robin by [email](mail
 to://robin.morisset@normalesup.org) if you will \nattend.\n\nModern mult
 iprocessor architectures and programming languages exhibit weakly \ncons
 istent memories. Their behaviour is formalised by the memory model of \n
 the architecture or programming language; it precisely defines which wri
 te \noperation can be returned by each shared memory read. This is not a
 lways the \nlatest store to the same variable, because of optimisations 
 in the \nprocessors such as speculative execution of instructions, the c
 omplex \neffects of caches, and optimisations made by compilers.\n\nIn t
 his thesis we focus on the C11 memory model that is defined by the 2011 
 \nedition of the C standard. Our contributions are threefold.\n\nFirst, 
 we focused on the theory surrounding the C11 model, formally studying \n
 which compiler optimisations it enables. We show that many common compil
 er \noptimisations are allowed, but, surprisingly, some important ones a
 re \nforbidden.\n\nSecondly, building on our results, we developed a ran
 dom testing methodology \nfor detecting when mainstream compilers such a
 s GCC or Clang perform an \nincorrect optimisation with respect to the m
 emory model. We found  several \nbugs in GCC, all promptly fixed. We als
 o implemented a novel optimisation \npass in LLVM, that looks for specia
 l instructions that restrict processor \noptimisations—called fence in
 structions—and eliminates the redundant ones.\n\nFinally, we developed
  a user-level scheduler for lightweight threads \ncommunicating through 
 first-in first-out single-producer single-consumer \nqueues. This progra
 mming model is known as Kahn process networks, and we \nshow how to effi
 ciently implement it, using C11 synchronisation primitives. \nThis shows
  that despite its flaws, C11 can be usable in practice.\n\nThe members o
 f the thesis committee are:\n\n* [Andrew Appel](https://www.cs.princeton
 .edu/~appel/),\n  Princeton University (Examiner)\n* [Mark Batty](https:
 //www.cs.kent.ac.uk/people/staff/mjb211/),\n  University of Kent\n* [Der
 ek Dreyer](https://people.mpi-sws.org/~dreyer/),\n  Max Planck Institute
  for Software Systems\n* [Doug Lea](http://gee.cs.oswego.edu/dl/index.ht
 ml),\n  State University of New York at Oswego (Examiner)\n* [Marc Pouze
 t](http://www.di.ens.fr/~pouzet/),\n  UPMC/ENS/Inria Paris\n* [Dmitry Vy
 ukov](http://www.1024cores.net),\n  Google\n* [Francesco Zappa Nardelli]
 (http://www.di.ens.fr/~zappa/),\n  Inria Paris (Director)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170313T150000
DTEND;TZID=Europe/Paris:20170313T173000
DTSTAMP;TZID=Europe/Paris:20170313T150000
UID:2017-03-13_Baudart
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Guillaume Baudart: A Synchronous Approach to Quasi-Periodic Syst
 ems
URL:http://parkas.di.ens.fr/seminars.html#2017-03-13_Baudart
DESCRIPTION:PhD thesis defense. The room is on the very top floor, see [
 this \nmap](http://gdt.ludics.eu/index.php/Salle_W).\nThere will be a 
 “pot-de-thèse” downstairs after the defense in\n[Salle S16](https:/
 /www.di.ens.fr/AccesDI.html.fr) in the Rataud Wing at the \nENS.\nThe [m
 anuscript](http://guillaume.baudart.eu/thesis/) and supporting \nmateria
 ls are available online.\n\nIn this thesis we study embedded controllers
  implemented as sets of \nunsynchronized periodic processes.\nEach proce
 ss activates quasi-periodically, that is, periodically with \nbounded ji
 tter, and communicates with bounded transmission delays.\nSuch reactive 
 systems, termed _quasi-periodic_, exist as soon as two \nperiodic proces
 ses are connected together.\nIn the distributed systems literature they 
 are also known as synchronous \nreal-time models.\nWe focus on technique
 s for the design and analysis of such systems without \nimposing a globa
 l clock synchronization.\n\nSynchronous languages were introduced as dom
 ain specific languages for the \ndesign of reactive systems.\nThey offer
  an ideal framework to program, analyze, and verify quasi-periodic \nsys
 tems.\nBased on a synchronous approach, this thesis makes contributions 
 to the \ntreatment of quasi-periodic systems along three themes: verific
 ation, \nimplementation, and simulation.\n\nVerification: The _quasi-syn
 chronous abstraction_ is a discrete abstraction \nproposed by Paul Caspi
  for model checking safety properties of \nquasi-periodic systems.\nWe s
 how that this abstraction is not sound in general and give necessary and
  \nsufficient conditions on both the static communication graph of the \
 napplication and the real-time characteristics of the architecture to re
 cover \nsoundness.\nWe then generalize these results to multirate system
 s.\n\nImplementation: _Loosely time-triggered architectures_ are protoco
 ls \ndesigned to ensure the correct execution of an application running 
 on a \nquasi-periodic system.\nWe propose a unified framework that encom
 passes both the application and the \nprotocol controllers.\nThis framew
 ork allows us to simplify existing protocols, propose optimized \nversio
 ns, and give new correctness proofs.\nWe instantiate our framework with 
 a protocol based on clock synchronization \nto compare the performance o
 f the two approaches.\n\nSimulation: Quasi-periodic systems are but one 
 example of timed systems \ninvolving real-time characteristics and toler
 ances.\nFor such nondeterministic models, we propose a _symbolic simulat
 ion_ scheme \ninspired by model checking techniques for timed automata.\
 nWe show how to compile a model mixing nondeterministic continuous-time 
 and \ndiscrete-time dynamics into a discrete program manipulating sets o
 f possible \nvalues.\nEach trace of the resulting program captures a set
  of possible executions of \nthe source program.\n\nThe members of the t
 hesis committee are:\n\n* [Albert Benveniste](http://people.rennes.inria
 .fr/Albert.Benveniste/),\n  Inria Rennes (Co-supervisor)\n* [Timothy Bou
 rke](http://www.tbrk.org),\n  Inria Paris (Supervisor)\n* [Nicolas Halbw
 achs](http://www-verimag.imag.fr/~halbwach/),\n  Vérimag (Reporter)\n* 
 [Marc Pouzet](https://www.di.ens.fr/~pouzet/),\n  ENS, UPMC, Inria Paris
  (Director)\n* [Xavier Rival](http://www.di.ens.fr/~rival/),\n  Inria Pa
 ris (Examiner)\n* [Alberto Sangiovanni-Vincentelli](http://people.eecs.b
 erkeley.edu/~alberto/),\n  University of California Berkeley (Examiner)\
 n* [Cesare Tinelli](http://homepage.cs.uiowa.edu/~tinelli/),\n  Universi
 ty of Iowa (Reporter)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170202T110000
DTEND;TZID=Europe/Paris:20170202T120000
DTSTAMP;TZID=Europe/Paris:20170202T110000
UID:2017-02-02_Beaugnon
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Ulysse Beaugnon: Optimization space pruning without regrets
URL:http://parkas.di.ens.fr/seminars.html#2017-02-02_Beaugnon
DESCRIPTION:Many computationally-intensive algorithms benefit from the w
 ide\nparallelism offered by Graphical Processing Units (GPUs). However, 
 the\nsearch for a close-to-optimal implementation remains extremely tedi
 ous due\nto the specialization and complexity of GPU architectures.\n\nW
 e present a novel approach to automatically discover the best performing
 \ncode from a given set of possible implementations. It involves a branc
 h\nand bound algorithm with two distinctive features: (1) an analytic\np
 erformance model of a lower bound on the execution time, and (2) the\nab
 ility to estimate such bounds on a partially-specified implementation.\n
 \nThe unique features of this performance model allow to aggressively pr
 une\nthe optimization space without eliminating the best performing\nimp
 lementation.  While the space considered in this paper focuses on GPUs,\
 nthe approach is generic enough to be applied to other architectures.\n\
 nWe implemented our algorithm in a tool called Telamon} and demonstrate 
 its\neffectiveness on a huge, architecture-specific and input-sensitive\
 noptimization space.\n\n\nThis will be a practice run for Ulysse's prese
 ntation at\n[CC 2017](http://conf.researchr.org/event/CC-2017/cc-2017-pa
 pers-optimization-space-pruning-without-regrets).\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20170127T110000
DTEND;TZID=Europe/Paris:20170127T120000
DTSTAMP;TZID=Europe/Paris:20170127T110000
UID:2017-01-27_Morisset
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Robin Morisset: Partially redundant fence elimination for x86, A
 RM and Power processors
URL:http://parkas.di.ens.fr/seminars.html#2017-01-27_Morisset
DESCRIPTION:We show how partial redundancy elimination (PRE) can be inst
 antiated to \nperform provably correct fence elimination for multi-threa
 ded programs \nrunning on top of the x86, ARM and IBM Power relaxed memo
 ry models.\nWe have implemented our algorithm in the backends of the LLV
 M compiler \ninfrastructure.\nThe optimisation does not induce an observ
 able overhead at compile-time and \ncan result in up-to 10% speedup on s
 ome benchmarks.\n\nThis will be a practice run for Robin and Francesco's
  presentation at\n[CC 2017](http://conf.researchr.org/event/CC-2017/cc-2
 017-papers-partially-redundant-fence-elimination-for-x86-arm-and-power-p
 rocessors).\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161209T140000
DTEND;TZID=Europe/Paris:20161209T153000
DTSTAMP;TZID=Europe/Paris:20161209T140000
UID:2016-12-09_MinhLe
LOCATION:salle Celan; 45 rue d'Ulm; ENS; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Nhat Minh Lê: Kahn Process Networks as Concurrent Data Structur
 es: Lock Freedom, Parallelism, Relaxation in Shared Memory
URL:http://parkas.di.ens.fr/seminars.html#2016-12-09_MinhLe
DESCRIPTION:PhD thesis defense. The room is on the ground floor, at numb
 er 14 on\n[this map](http://www.ens.fr/IMG/pdf/Plan_45ULM_RDC.pdf).\n\nI
 n this thesis, we are interested in Kahn process networks, a simple\nyet
  expressive model of concurrency, and its parallel implementation\non mo
 dern shared-memory architectures. Kahn process networks expose\nconcurre
 ncy to the programmer through an arrangement of sequential\nprocesses an
 d single-producer single-consumer channels.\n\nThe focus is on the imple
 mentation aspects. Of particular importance\nto our study are two parame
 ters: lock freedom and relaxed memory. The\ndevelopment of fast and effi
 cient lock-free algorithms ties into\nconcerns of controlled resource co
 nsumption (important in embedded\nsystems) and reliable performance on c
 urrent and future platforms with\nunfair or skewed scheduling such as vi
 rtual machines and GPUs. Our\nwork with relaxed memory models complement
 s this more theoretical\napproach by offering a window into realistic sh
 ared-memory\narchitectures.\n\nWe present a new lock-free algorithm for 
 a Kahn process network\ninterpreter. It is disjoint-access parallel: we 
 allow multiple threads\nto work on the same shared Kahn process network,
  fully utilizing the\nparallelism exhibited by independent processes. It
  is non-blocking in\nthat it guarantees global progress in bounded memor
 y, even in the\npresence of (possibly infinite) delays affecting the exe
 cuting\nthreads. To our knowledge, it is the first lock-free system of t
 his\nsize, and integrates various well-known non-blocking techniques and
 \nconcepts (e.g., safe memory reclamation, multi-word updates,\nassistan
 ce) with ideas and optimizations specific to the Kahn network\nsetting. 
 We also discuss a blocking variant of this algorithm,\ntargetted at high
 -performance computing, with encouraging experimental\nresults.\n\nThe m
 embers of the thesis committee are:\n\n* [Albert Cohen](https://who.rocq
 .inria.fr/Albert.Cohen/),\n  Inria Paris (Directeur)\n* [Mike Dodds](htt
 ps://www-users.cs.york.ac.uk/~miked/),\n  University of York (Rapporteur
 )\n* [Alastair F. Donaldson](http://multicore.doc.ic.ac.uk),\n  Imperial
  College (Examinateur)\n* [Tim Harris](https://timharris.uk),\n  Oracle 
 Labs Cambridge (Examinateur)\n* [Francesco Zappa Nardelli](http://www.di
 .ens.fr/~zappa/),\n  Inria Paris (Président)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161124T140000
DTEND;TZID=Europe/Paris:20161124T150000
DTSTAMP;TZID=Europe/Paris:20161124T140000
UID:2016-11-24_Rajopadhye
LOCATION:salle Aimé Césaire; 2ème escalier A; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Sanjay Rajopadhye: Thirty Years of the Polyhedral Model and Wher
 e are We?
URL:http://parkas.di.ens.fr/seminars.html#2016-11-24_Rajopadhye
DESCRIPTION:Even after thirty years, the polyhedral model is far from be
 ing an unequivocal success, even on the restricted domain where it is ap
 plicable.  We do not (yet) have compilers for general-purpose processors
  that can generate code approaching either the machine peak, or the algo
 rithmic peak of the source program, or hand tuned libraries developed by
  “heroes of high performance computing.”  I will try to explain why 
 this is so, and suggest a plan of how we can improve this state of affai
 rs.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161107T110000
DTEND;TZID=Europe/Paris:20161107T120000
DTSTAMP;TZID=Europe/Paris:20161107T110000
UID:2016-11-07_Pai
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Sreepathi Pai: A Compiler for Throughput Optimization of Graph P
 rograms on GPUs
URL:http://parkas.di.ens.fr/seminars.html#2016-11-07_Pai
DESCRIPTION:Graphics Processing Units (GPUs) are an attractive target fo
 r graph\nalgorithms because they support massively parallel execution an
 d\npossess much higher memory bandwidths than CPUs and FPGAs. However,\n
 graph programs are also highly irregular and low-level GPU programming\n
 models make writing high-performance implementations very challenging.\n
 \nIn this talk, I will describe the Galois GPU compiler that we have\nbu
 ilt to generate high-performance implementations of graph\nalgorithms on
  GPUs. Beginning with a high-level representation of\ngraph algorithms, 
 which we call IrGL, our compiler generates\noptimized CUDA code for NVID
 IA GPUs by applying three key\noptimizations that I argue are fundamenta
 l to high-performance\nimplementations of graph algorithms on GPUs. Eval
 uation on eight\ngraph applications shows that our compiler produces cod
 e that\noutperforms all current state-of-the-art handwritten CUDA\nimple
 mentations.\n\nGraph program performance strongly depends on the inputs,
  and this\nmakes picking the right set of optimizations for a given inpu
 t very\ndifficult. We show how our compiler can exploit queuing network\
 nmodels generated from IrGL source code to customize optimizations\nfor 
 combinations of applications and inputs.\n\nParts of this work will appe
 ar in OOPSLA 2016.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161027T100000
DTEND;TZID=Europe/Paris:20161027T110000
DTSTAMP;TZID=Europe/Paris:20161027T100000
UID:2016-10-27_Janin
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:David Janin: Semantic models for timed programing languages
URL:http://parkas.di.ens.fr/seminars.html#2016-10-27_Janin
DESCRIPTION:In this talk, I consider temporally causal functions of time
 d streams, i.e., \nfunctions that produce output values at a given insta
 nt that only depend on \nthe input values that have been received till t
 hat instant. Defining partial \ntimed streams that form a directed compl
 ete partial order (DCPO), I will \nshow how causal functions are nicely 
 captured as limits of continuous and \nsynchronous functions over these 
 DCPO offering thus a denotational model of \ncausal timed functions. Rel
 axing the synchronous hypothesis to a \npre-synchronous hypothesis, I wi
 ll show how every causal function admits a \nlattice of possible denotat
 ions such that:\n\n  * the least element can be understood as the latest
  semantics of that \n    function: output values are computed when they 
 need to be outputted,\n  * the greatest element can be understood as the
  earliest semantics of that \n    function: output values are computed a
 s soon as all the input values \n    they depend have been received.\n  
 * other elements in between can be understood as the various possible \n
     computation schedules that can still be followed in order to run the
  \n    causal function.\n\nThe categorical properties of these continuou
 s functions will then be \ndetailed, offering various relevant operators
  for programing with them.\nLastly, I will show that a notion of causal 
 function residual is available \nso that a minimal (possibly continuous)
  IO-automaton can be associated to \nevery causal function, providing th
 us an abstract operational (latest) \nsemantics. Open perspectives and q
 uestions will conclude this presentation.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161018T110000
DTEND;TZID=Europe/Paris:20161018T120000
DTSTAMP;TZID=Europe/Paris:20161018T110000
UID:2016-10-18_Champion
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Adrien Champion: Kind 2: Contract-based Compositional Reasoning
URL:http://parkas.di.ens.fr/seminars.html#2016-10-18_Champion
DESCRIPTION:Contract-based software development is a leading methodology
  for the \nconstruction of safety- and mission-critical embedded systems
 . Contracts are \nan effective way to establish boundaries between compo
 nents and can be used \nefficiently to verify global properties by using
  compositional reasoning \ntechniques. A contract specifies the assumpti
 ons a component makes on its \ncontext and the guarantees it provides. R
 equirements in the specification of \na component are often case-based, 
 with each case describing what the \ncomponent should do depending on a 
 specific situation (or mode) the \ncomponent is in. This talk introduces
  CoCoSpec, a mode-aware \nassume-guarantee-based contract language for e
 mbedded systems built as an \nextension of the Lustre language. CoCoSpec
  lets users specify mode behavior \ndirectly, instead of encoding it as 
 conditional guarantees, thus preventing \na loss of mode-specific inform
 ation. Mode-aware model checkers supporting \nCoCoSpec can increase the 
 effectiveness of the compositional analysis \ntechniques found in assume
 -guarantee frameworks and improve scalability. \nSuch tools can also pro
 duce much better feedback during the verification \nprocess, as well as 
 valuable qualitative information on the contract itself. \nI will presen
 ts the CoCoSpec language and illustrate the benefits of \nmode-aware mod
 el-checking on a case study involving a flight-critical \navionics syste
 m. The evaluation uses [Kind 2][1], a collaborative, parallel, \nSMT-bas
 ed model checker developed at the University of Iowa that provides \nful
 l support for CoCospec. \n\n[1]: https://github.com/kind2-mc\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161018T100000
DTEND;TZID=Europe/Paris:20161018T110000
DTSTAMP;TZID=Europe/Paris:20161018T100000
UID:2016-10-18_Bekooij
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Marco Bekooij: A Refinement Theory for Timed-Dataflow Analysis w
 ith Support for Reordering
URL:http://parkas.di.ens.fr/seminars.html#2016-10-18_Bekooij
DESCRIPTION:Real-time stream processing applications executed on embedde
 d multiprocessor systems often have strict throughput and latency constr
 aints. Violating these constraints is undesired and temporal analysis me
 thods are therefore used to prevent such violations. These analysis meth
 ods use abstractions of the analyzed applications to simplify their temp
 oral analysis.\n\nRefinement theories have enabled the creation of deter
 ministic abstractions of stream processing applications that are execute
 d on multiprocessor systems. Prominent examples of such abstract models 
 are deterministic timed-dataflow models which can be efficiently analyze
 d because they only have one behavior.\n\nAn important aspect of a strea
 m processing application can be that it makes use of reordered data stre
 ams between tasks. An example is the bit-reversed ordered stream produce
 d by a FFT task. Another example is reordering that is a result of data-
 parallelism. However, existing abstraction/refinement theories do not su
 pport such reordering behavior or do not handle this type of behavior co
 rrectly. This is because existing refinement theories assume that the te
 mporal behavior of applications is orthogonal to their functional behavi
 or, whereas this orthogonality does not always hold in the case of reord
 ered data streams.\n\nIn this talk I will present a new refinement theor
 y in which the potential interaction between temporal and functional beh
 avior is taken into account. The introduced theory supports reordering o
 f data and can therefore be used to validate existing systems with such 
 reordering. Furthermore, the theory enables showing that deterministic d
 ataflow models that do not apply reordering can be used as valid abstrac
 tions of systems in which reordering takes place.\n\nNote 1: Marco will 
 also serve on the thesis committee of Khanh Xuan Do, CEA List, NanoInnov
 , Monday October 17 at 14:30.\n\nNote 2: we will continue with the semin
 ar of Adrien Champion in the same room after a short coffee break.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20161014T163000
DTEND;TZID=Europe/Paris:20161014T173000
DTSTAMP;TZID=Europe/Paris:20161014T163000
UID:2016-10-14_Mandel
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Louis Mandel: A Compiler Driver in Coq / Un gestionnaire de chem
 ins de compilation en Coq
URL:http://parkas.di.ens.fr/seminars.html#2016-10-14_Mandel
DESCRIPTION:[Q*cert][1]  is a query compiler written in Coq. Initially d
 edicated to the \ncompilation of jRule to Cloudant, it is now able to co
 mpile several source \nlanguages (e.g., OQL, NRA) and to generate code f
 or Java or Spark. \nInternally, Q*cert uses 14 languages and 27 unitary 
 translation functions to \ngo directly from one language to another. In 
 this talk, I will present how \nwe handle all these compilation paths an
 d how proofs help to maintain the \noptions of the command line compiler
 .\n\nJoint work with Joshua Auerbach, Martin Hirzel, Avraham Shinnar and
 \nJérôme Siméon.\n\n* * *\n\n[Q*cert][1] est un compilateur de requê
 tes écrit en Coq. Initialement dédié \nà la compilation de jRule ver
 s Cloudant, il est maintenant capable de \ncompiler plusieurs langages s
 ources (e.g., OQL, NRA) et de générer du code \npour Java ou Spark. En
  interne, Q*cert utilise 14 langages et 27 fonctions \nde traductions un
 itaires permettant de passer directement d'un langage à un \nautre. Dan
 s cet exposé, je présenterai comment nous faisons pour gérer tous \nc
 es chemins de compilation et comment les preuves nous aident à mainteni
 r à \njour les options de la ligne de commande du compilateur.\n\nTrava
 il réalisé en collaboration avec Joshua Auerbach, Martin Hirzel,\nAvra
 ham Shinnar et Jérôme Siméon.\n\n[1]: https://querycert.github.io/\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160930T130000
DTEND;TZID=Europe/Paris:20160930T140000
DTSTAMP;TZID=Europe/Paris:20160930T130000
UID:2016-09-30_Iooss
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Guillaume Iooss: Detection of Linear Algebra Operations in Polyh
 edral Programs
URL:http://parkas.di.ens.fr/seminars.html#2016-09-30_Iooss
DESCRIPTION:Writing code which uses an architecture at its full capabili
 ty has become an \nincreasingly difficult problem. For some key operatio
 ns, a dedicated \naccelerator or a finely tuned implementation exists an
 d delivers the best \nperformance. When compiling code, identifying thes
 e operations and issuing \ncalls to their high-performance implementatio
 ns is thus attractive. In this \ntalk, we focus on the problem of detect
 ing such operations. We propose a \nframework which detects linear algeb
 ra subcomputations within a polyhedral \nprogram. The main idea of this 
 framework is to partition the computation in \norder to isolate differen
 t subcomputations in a regular manner, then we \nconsider each portion o
 f the computation and try to recognize it as a \ncombination of linear a
 lgebra operations.\n\nWe perform the partitioning of the computation by 
 using a program \ntransformation called monoparametric tiling. This tran
 sformation partitions \nthe computation into blocks, whose shape is some
  homothetic scaling of a \nfixed-size partitioning. We show that the til
 ed program remains polyhedral \nwhile allowing a limited amount of param
 etrization: a single size parameter. \nThis is an improvement compared t
 o the previous work on tiling, that forced \na choice between these two 
 properties.\n\nThen, in order to recognize computations, we introduce a 
 template \nrecognition algorithm built built on a state-of-the-art progr
 am equivalence \nalgorithm. We also propose several extensions in order 
 to manage some \nsemantic properties.\n\nFinally, we combine these two c
 ontributions into a framework which detects \nlinear algebra subcomputat
 ions. A part of this framework is a library of \ntemplates based on the 
 BLAS specification. We demonstrate our framework on \nseveral applicatio
 ns.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160817T103000
DTEND;TZID=Europe/Paris:20160817T120000
DTSTAMP;TZID=Europe/Paris:20160817T103000
UID:2016-08-17_Amarasinghe
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Saman Amarasinghe: Halide and Simit: Domain Specific Languages w
 hen Performance Matters
URL:http://parkas.di.ens.fr/seminars.html#2016-08-17_Amarasinghe
DESCRIPTION:Achieving high performance is no easy task. From the early d
 ays of\ncomputing, many researchers have spent their lifetime trying to 
 extract more\nFLOPS out of critical codes.  Hardcore performance enginee
 rs try to get to\nthis performance nirvana single handedly without any h
 elp from languages,\ncompilers or tools. In this talk I'll argue that pr
 ogramming languages and\ncompiler technology can take on most of the per
 formance optimization\nburden... at least in certain domains.\nWe will d
 emonstrate the performance optimization ability of compilers and\nlangua
 ges in the domains of image processing and physical simulation. Most\nth
 ese applications are performance critical, and programmers spend many\nm
 onths optimizing them.\nIn the first part of this talk, I will describe 
 Halide, a language and\ncompiler for image processing. Halide explicitly
  separates the description\nof the algorithm, the task of the domain exp
 ert, from the choices of\nexecution structure which determine parallelis
 m, locality, memory footprint,\nand synchronization, the domain of the p
 erformance engineer. We show how\nthis separation simplifies the problem
  for both the domain expert and the\nperformance engineer. Using machine
  learning we can even eliminate the\nperformance engineer entirely from 
 the process. The end result is much\nsimpler programs, delivering perfor
 mance often many times faster than the\nbest prior hand-tuned C, assembl
 y, and CUDA implementations, while scaling\nacross radically different a
 rchitectures, from ARM cores to massively\nparallel GPUs.\n\nIn the seco
 nd part of the talk, I will introduce Simit, a new language for\nphysica
 l simulations. Simit lets the programmer seamlessly work on a\nphysical 
 system both in its individual geometric elements as a hypergraph as\nwel
 l as the behavior of the entire system as set of global tensors. Simit\n
 provides a novel assembly construct that makes it conceptually easy and\
 ncomputationally efficient to move between these two abstractions. Using
  the\ninformation provided by the assembly construct, the compiler gener
 ates\nefficient in-place computation on the graph. We demonstrate that S
 imit is\neasy to use: a Simit program is typically shorter than a Matlab
  program;\nthat it is high performance: a Simit program running sequenti
 ally on a CPU\nperforms comparably to hand-optimized simulations; and th
 at it is portable:\nSimit programs can be compiled for GPUs with no chan
 ge to the program,\ndelivering 4 to 20x speedups over our optimized CPU 
 code.\n\nBio: Saman P. Amarasinghe is a Professor in the Department of E
 lectrical\nEngineering and Computer Science at Massachusetts Institute o
 f Technology\nand a member of the Computer Science and Artificial Intell
 igence Laboratory\n(CSAIL) where he leads the Commit compiler group. Und
 er Saman's guidance,\nthe Commit group has developed the StreamIt, PetaB
 ricks, StreamJIT, Halide,\nSimit, and MILK programming languages and com
 pilers, DynamoRIO dynamic\ninstrumentation system, Superword level paral
 lelism for SIMD vectorization,\nProgram Shepherding to protect programs 
 against external attacks, the\nOpenTuner extendable autotuner, and the K
 endo deterministic execution\nsystem. He was the co-leader of the Raw ar
 chitecture project. His research\ninterests are in discovering novel app
 roaches to improve the performance of\nmodern computer systems and make 
 them more secure without unduly increasing\nthe complexity faced by the 
 end users, application developers, compiler\nwriters, or computer archit
 ects. Saman was the founder of Determina\nCorporation and a co-founder o
 f Lanka Internet Services Ltd. Saman received\nhis BS in Electrical Engi
 neering and Computer Science from Cornell\nUniversity in 1988, and his M
 SEE and Ph.D from Stanford University in 1990\nand 1997, respectively. 
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160623T130000
DTEND;TZID=Europe/Paris:20160623T140000
DTSTAMP;TZID=Europe/Paris:20160623T130000
UID:2016-06-23_GallegoArias
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Emilio J. Gallego Arias: Experiments in Certified Digital Audio 
 Processing
URL:http://parkas.di.ens.fr/seminars.html#2016-06-23_GallegoArias
DESCRIPTION:We will present recent developments in Wagner, a functional\
 nprogramming language geared towards real-time digital audio\nprocessing
  with formal, machine-checkable semantics.\n\nWagner can be seen as eith
 er a very simple synchronous language of a\nfunctional reactive one, usi
 ng coeffects for history tracking,\nallowing a natural coding of filter 
 and digital waveguide\noscillators.\n\nIn order to relate programs with 
 their mathematical model three main\ncomponents are needed:\n\n1. A Coq 
 library with some facts about the Discrete Fourier Transform and \n   un
 itary transforms. The formalization is constructive and heavily relies \
 n   on the Mathematical Components library.\n\n2. An embedding of Wagner
  into Coq, crucially allowing a lightweight \n   mechanization style as 
 we can reuse most of Mathcomp's linear algebra \n   libraries. The funct
 ional nature of Wagner allows the use of typical PL \n   techniques such
  as for example logical relations to characterize the \n   subset of Wag
 ner programs that are “linear processors”.\n\n3. Finally, a call-by-
 value abstract machine with a heap provides the \n   efficient execution
  model. Basic ideas from the focusing literature are \n   used to distin
 guish “positive” and “negative” types.\n\n   We embed the machin
 e in Coq using the standard monadic CBV translation \n   and we link it 
 to the semantics in 2) by relating well-formed heaps with \n   typing en
 vironments.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160613T110000
DTEND;TZID=Europe/Paris:20160613T120000
DTSTAMP;TZID=Europe/Paris:20160613T110000
UID:2016-06-13_Talbot
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Pierre Talbot: Spacetime Programming
URL:http://parkas.di.ens.fr/seminars.html#2016-06-13_Talbot
DESCRIPTION:Search heuristics are of utter importance for solving Constr
 aint \nSatisfaction Problems (CSP) efficiently. However, the implementer
 s will \nstruggle to choose between a full-fledged but low-level constra
 int library \nor high-level languages proposing a limited amount of pre-
 built heuristics. \nWe introduce Spacetime Programming (STP), a paradigm
  based on concurrent \nconstraint programming and synchronous languages,
  where both time and space \nare part of the language. The variables are
  characterized by a “spacetime”\nproperty describing how their value
 s evolve through time and space. We will \npresent preliminary work demo
 nstrating how STP, in the context of CSP \nsolving, can be used for writ
 ing and composing search strategies.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160606T150000
DTEND;TZID=Europe/Paris:20160606T160000
DTSTAMP;TZID=Europe/Paris:20160606T150000
UID:2016-06-06_Sjolund
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Martin Sjölund: Tools and Methods for Analysis, Debugging, and 
 Performance Improvement of Equation-Based Models
URL:http://parkas.di.ens.fr/seminars.html#2016-06-06_Sjolund
DESCRIPTION:Equation-based object-oriented (EOO) modeling languages such
  as Modelica\nprovide a convenient, declarative method for describing mo
 dels of\ncyber-physical systems. Because of the ease of use of EOO langu
 ages, large\nand complex models can be built with limited effort.\n\nHow
 ever, current state-of-the-art tools do not provide the user with enough
 \ninformation when errors appear or simulation results are wrong. It is 
 of\nparamount importance that such tools should give the user enough inf
 ormation\nto correct errors or understand where the problems that lead t
 o wrong\nsimulation results are located. However, understanding the mode
 l translation\nprocess of an EOO compiler is a daunting task that not on
 ly requires\nknowledge of the numerical algorithms that the tool execute
 s during\nsimulation, but also the complex symbolic transformations bein
 g performed.\n\nAs part of this work, methods have been developed and ex
 plored where the EOO\ntool, an enhanced Modelica compiler, records the t
 ransformations during the\ntranslation process in order to provide bette
 r diagnostics, explanations,\nand analysis. This information is used to 
 generate better error-messages\nduring translation. It is also used to p
 rovide better debugging for a\nsimulation that produces unexpected resul
 ts or where numerical methods fail.\n\nMeeting deadlines is particularly
  important for real-time applications. It\nis usually essential to ident
 ify possible bottlenecks and either simplify\nthe model or give hints to
  the compiler that enable it to generate faster\ncode. When profiling an
 d measuring execution times of parts of the model the\nrecorded informat
 ion can also be used to find out why a particular system\nmodel executes
  slowly.\n\nCombined with debugging information, it is possible to find 
 out why this\nsystem of equations is slow to solve, which helps understa
 nding what can be\ndone to simplify the model. A tool with a graphical u
 ser interface has been\ndeveloped to make debugging and performance prof
 iling easier. Both debugging\nand profiling have been combined into a si
 ngle view so that performance\nmetrics are mapped to equations, which ar
 e mapped to debugging information.\n\nThe algorithmic part of Modelica w
 as extended with meta-modeling constructs\n(MetaModelica) for language m
 odeling. In this context a quite general\napproach to debugging and comp
 ilation from (extended) Modelica to C code was\ndeveloped. That makes it
  possible to use the same executable format for\nsimulation executables 
 as for compiler bootstrapping when the compiler\nwritten in MetaModelica
  compiles itself.\n\n_Bio:_ Martin Sjölund is doing a postdoc at Linkö
 ping University where he\nfinished his PhD in 2015. The thesis is mostly
  focused on debugging\nand profiling of an equation-based object-oriente
 d (EOO) language called\nModelica. He has worked on various parts of the
 \n[OpenModelica](https://openmodelica.org/) compiler since 2009, both do
 ing\nresearch  (resulting in the PhD) and development work for the Open 
 Source\nModelica Consortium (resulting in improved portability, performa
 nce,\nscalability, and new features in OpenModelica).\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160601T140000
DTEND;TZID=Europe/Paris:20160601T150000
DTSTAMP;TZID=Europe/Paris:20160601T140000
UID:2016-06-01_Zinenko
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Oleksandr Zinenko: Polyhedral program transformations via intera
 ctive visualization
URL:http://parkas.di.ens.fr/seminars.html#2016-06-01_Zinenko
DESCRIPTION:_Context:_ part of the PhD thesis work of Oleksandr Zinenko.
 \n\nThe Polyhedral model is a powerful framework for program\ntransforma
 tion, yet it remains complex for direct use, even by\nexperts.  We lever
 age the inherent geometric nature of the model to\nvisualize programs an
 d to support code transformation by directly\nmanipulating these visuali
 zations with automatic code generation and\nfeedback on semantics preser
 vation.  Besides manual transformation, the\nuser of our interactive too
 l, Clint, is able to recover, visually\nreplay and adjust an automatical
 ly computed optimization using a set\nof syntactic-level directives with
  strong semantics.  Combining this\nvisualization with existing polyhedr
 al tools introduces visual aid for\nschedule and transformation construc
 tion.  Empirical user studies\ndemonstrated that visual representations 
 allow to extract and express\nparallelism faster and with more success.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160412T103000
DTEND;TZID=Europe/Paris:20160412T120000
DTSTAMP;TZID=Europe/Paris:20160412T103000
UID:2016-04-12_Llopard
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Ivan Llopard: Programming Embedded Manycore: Refinement and Opti
 mizing Compilation of a Parallel Action Language for Hierarchical State 
 Machines
URL:http://parkas.di.ens.fr/seminars.html#2016-04-12_Llopard
DESCRIPTION:Context: presentation of the PhD thesis work of Ivan Llopard
 ; the\nthesis was prepared at CEA Leti and will be defended on April 26t
 h in\nGrenoble.\n\nModeling languages propose convenient abstractions an
 d transformations\nto harness the complexity of today's embedded systems
 .  These\nlanguages are often based on the formalism of Hierarchical Sta
 te\nMachines, such as the widely known Statecharts.  While they naturall
 y\ncapture the concurrency of control systems, they face two important\n
 challenges when it comes to modeling data-intensive applications on\nmod
 ern parallel architectures: the absence of a unified approach that\nalso
  accounts for (data) parallel actions; and the lack of an\neffective opt
 imization and code generation flow. We propose a modeling\nlanguage exte
 nded with parallel action semantics and indexed state\nmachines suitable
  for computationally intensive applications. Together\nwith its formal s
 emantics, we present an optimizing compiler aiming\nfor the generation o
 f efficient parallel implementations. Following a\nmodel-driven methodol
 ogy, the compilation flow has been successfully\napplied to manycore arc
 hitectures such as GPGPU platforms.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160401T130000
DTEND;TZID=Europe/Paris:20160401T140000
DTSTAMP;TZID=Europe/Paris:20160401T130000
UID:2016-04-01_Bodin
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Bruno Bodin: Performance analysis of dataflow models
URL:http://parkas.di.ens.fr/seminars.html#2016-04-01_Bodin
DESCRIPTION:Synchronous Dataflow graphs, an equivalent of weighted petri
 -nets\nintroduced by Lee and Messerschmitt in 1987, is a well-known form
 alism\ncommonly used to model data-exchanges between parallel programs. 
 This\nmodel has been extensively studied in the last two decades because
  of\nthe importance of its applications. However, the determination of a
 \nmaximal throughput is a difficult question, for which no polynomial\nt
 ime algorithm exists up to now.  Several authors proved that it\nexists 
 a schedule which reaches the maximum throughput but with a no\npolynomia
 lly bounded size. On the other hand a strictly periodic\nschedule may be
  built polynomially, but without any guarantee on the\nthroughput achiev
 ed.  In this context, we investigate the trade-off\nbetween schedules si
 ze and their corresponding\nthroughput. Additionally, the applicability 
 of these models on SLAM\nalgorithms is explored.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160316T170000
DTEND;TZID=Europe/Paris:20160316T180000
DTSTAMP;TZID=Europe/Paris:20160316T170000
UID:2016-03-16_Raymond
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Pascal Raymond: Analyse de pire temps d'exécution et programmat
 ion synchrone
URL:http://parkas.di.ens.fr/seminars.html#2016-03-16_Raymond
DESCRIPTION:[Séminaire du DI](http://www.di.ens.fr/SeminaireGeneral.htm
 l.fr#Mercredi_16_mars_2016_17h00_Pasc).\n\nLes systèmes embarqués sont
  des dispositifs informatisés dédiés à une tâche \nspécifique, typ
 iquement le contrôle/commande d'un processus physique. On en \ntrouve d
 ans le domaine des transports (freinage assisté, allumage moteur, \ncom
 mande de vol), du contrôle de processus industriel, ou de la production
  \nd'énergie. Les termes de systèmes réactifs, systèmes temps-réel 
 (dur) \ncouvrent à peu près la même réalité.\n\nUne caractéristiqu
 e principale de ces systèmes est la criticité : les \ndéfaillances pe
 uvent être catastrophiques. Il faut donc s'assurer de la \ncorrection d
 e ses systèmes avant leur mises en service.\n\nPour être considéré c
 omme correct, un tel système doit essentiellement : - \ncalculer juste
  : il réalise bien la fonctionnalité attendue, sans bogue de \nconcept
 ion ni erreur à l'exécution ; - calculer (suffisamment) vite : la \nvi
 tesse de réaction du système doit être en adéquation avec la dynamiq
 ue du \nprocessus physique qu'il contrôle.\n\nL'approche synchrone, for
 malisée dans le courant des années 80, s'intéresse \nspécifiquement 
 aux aspects fonctionnels. Elle propose un cadre idéalisé pour \nla con
 ception des systèmes (concurrence déterministe), et fournit les outils
  \nnécessaires pour la programmation, la validation, la compilation et 
 \nl'implantation du logiciel embarqué. L'outil Scade (Esterel technolog
 ies) \nest un exemple typique d'un environnement de programmation synchr
 one, \nutilisé en production dans l'industrie (commandes de vol Airbus 
 et bien \nautres).\n\nL'analyse temporelle cherche à vérifier que le t
 emps de réaction du système \nimplanté est conforme aux contraintes t
 emps-réel de son environnement. Aux \nméthodes dynamiques classiques, 
 basées sur le test et la mesure, se sont \najoutées à partir des ann
 ées 90 des méthodes d'analyse statiques qui \ncherchent à déterminer
  des bornes supérieures garanties aux temps de \nréaction. Le problèm
 e de base de ces méthodes est l'estimation du pire temps \nd'exécution
  d'un code séquentiel donné sur une architecture donnée (Worst \nCase
  Execution Time, ou WCET).\n\nCet exposé présente les complémentarit
 és des deux domaines, puis aborde plus \nspécifiquement des travaux r
 écents qui visent à analyser la sémantique des \nprogrammes synchrone
 s pour découvrir des chemins d'exécutions infaisables \nsur le code co
 mpilé, et donc, potentiellement, d'affiner les estimations de \npire te
 mps d'exécution.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160113T170000
DTEND;TZID=Europe/Paris:20160113T180000
DTSTAMP;TZID=Europe/Paris:20160113T170000
UID:2016-01-13_Pagano
LOCATION:salle Henri Cartan; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Bruno Pagano: Scade 6: Conception d'un langage de programmation 
 synchrone et réalisation de son compilateur pour les systèmes embarqu
 és critiques
URL:http://parkas.di.ens.fr/seminars.html#2016-01-13_Pagano
DESCRIPTION:[Séminaire du DI](http://www.di.ens.fr/SeminaireGeneral.htm
 l.fr#Mercredi_13_janvier_2016_17h00_B).\n\nDans le contexte des système
 s embarqués critiques, l'objectif principal du logiciel n'est pas d'eff
 ectuer des calculs extrêmement longs et complexes à partir d'une donn
 ée qui lui est fournie initialement, mais de réagir de façon sure et 
 déterministe aux évènements externes qui lui sont communiqués de man
 ière régulière tout au long de son exécution. La réalisation de tel
 s logiciels peut se faire en utilisant des langages de programmation dé
 diés dont la conception et les techniques de compilation sont un sujet 
 de recherche actif depuis une trentaine d'années. Les langages de progr
 ammation synchrones, comme Esterel ou Lustre, ont prouvé leur utilité 
 dans la réalisation des systèmes réactifs. Après une introduction au
 x principes des langages synchrones, cet exposé présentera à travers 
 le langage de programmation Scade 6 (dialecte de Lustre) les travaux de 
 recherche d'Esterel Technologies sur la réalisation et la compilation d
 'un langage textuel et graphique. Nous évoquerons les mécanismes parti
 culiers à Scade qui ont été introduit ainsi qu'un travail en cours su
 r l'utilisation de Scade pour la simulation de systèmes physiques.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160113T104500
DTEND;TZID=Europe/Paris:20160113T114500
DTSTAMP;TZID=Europe/Paris:20160113T104500
UID:2016-01-13_Beaugnon
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Ulysse Beaugnon: A Quest for the Optimal Matrix-Matrix Multiplic
 ation Code
URL:http://parkas.di.ens.fr/seminars.html#2016-01-13_Beaugnon
DESCRIPTION:Finding a near-optimal implementation of a program on a GPU 
 is a daunting task. The programmer or the compiler must not only explore
  regular code optimizations but also handle the placement of the data in
  the memory hierarchy and choose a parallelism scheme. The solution we p
 ropose explores a set of possible implementation to find the optimal one
  for a given input and GPU model. The problem with this approach is that
  the search space has an exponential size. We thus propose a performance
  model to trim the search space and drive the search.\n\nThe seminar is 
 based on the work conducted during an internship at Google.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20160107T103000
DTEND;TZID=Europe/Paris:20160107T120000
DTSTAMP;TZID=Europe/Paris:20160107T103000
UID:2016-01-07_Guatto
LOCATION:salle Jean Jaurès; 29 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Adrien Guatto: A Synchronous Functional Language with Integer Cl
 ocks
URL:http://parkas.di.ens.fr/seminars.html#2016-01-07_Guatto
DESCRIPTION:PhD thesis defense.\n\nThis thesis addresses the design and 
 implementation of a\nprogramming language for real-time stream processin
 g\napplications, such as video decoding. The model of Kahn process\nnetw
 orks is a natural fit for this area and has been used\nextensively. In t
 his model, a program consists in a set of\nparallel processes communicat
 ing through single reader, single\nwriter queues. The strength of the mo
 del lies in its determinism.\n\nSynchronous functional languages like Lu
 stre are dedicated to\ncritical embedded systems. A Lustre program defin
 es a Kahn\nprocess network which is synchronous, that is, which can be\n
 executed with finite queues and without deadlocks. This is\nenforced by 
 a dedicated type system, the clock calculus, which\nestablishes a global
  time scale throughout a program. The global\ntime scale is used to defi
 ne clocks: per-queue boolean sequences\nindicating, for each time step, 
 whether a process produces or\nconsumes a token in the queue. This infor
 mation is used both for\nenforcing synchrony and for generating finite-s
 tate software or\nhardware.\n\nWe propose and study integer clocks, a ge
 neralization of boolean\nclocks featuring arbitrarily big natural number
 s. Integer clocks\ndescribe the production or consumption of several val
 ues from the\nsame queue in the course of a time step. We then rely on i
 nteger\nclocks to define the local time scale construction, which may\nh
 ide time steps performed by a sub-program from the surrounding\ncontext.
   These principles are integrated into a clock calculus\nfor a higher-or
 der functional language. We study its properties,\nproving among other t
 hings that well-typed programs do not\ndeadlock. We compile typed progra
 ms to digital synchronous\ncircuits by adapting the clock-directed code 
 generation scheme of\nLustre. The typing information controls certain tr
 ade-offs\nbetween time and space in the generated circuits.\n\nThe membe
 rs of the thesis committee are:\n\n* [Gérard Berry](http://www.college-
 de-france.fr/site/gerard-berry),\n  Collège de France (Président)\n* [
 Mary Sheeran](http://www.cse.chalmers.se/~ms),\n  Chalmers University (R
 apporteur)\n* [Robert de Simone](http://www-sop.inria.fr/members/Robert.
 De_Simone),\n  INRIA Nice - Sophia Antipolis (Rapporteur)\n* [Stephen Ed
 wards](http://www.cs.columbia.edu/~sedwards),\n  Columbia University (Ex
 aminateur)\n* [Dan R. Ghica](http://www.cs.bham.ac.uk/~drg),\n  Birmingh
 am University (Examinateur)\n* [Albert Cohen](https://who.rocq.inria.fr/
 Albert.Cohen),\n  INRIA Rocquencourt (Directeur de thèse)\n* [Marc Pouz
 et](http://www.di.ens.fr/~pouzet),\n  ENS et Université Paris 6 (Codire
 cteur de thèse)\n* [Louis Mandel](https://www.lri.fr/~mandel),\n  IBM R
 esearch (Encadrant)\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150929T110000
DTEND;TZID=Europe/Paris:20150929T120000
DTSTAMP;TZID=Europe/Paris:20150929T110000
UID:2015-09-29_Baudard
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Guillaume Baudard: Loosely Time-Triggered Architectures: Improve
 ments and Comparisons
URL:http://parkas.di.ens.fr/seminars.html#2015-09-29_Baudard
DESCRIPTION:Loosely Time-Triggered Architectures (LTTAs) are a proposal 
 for\nconstructing distributed embedded control systems. They build on th
 e\nquasi-periodic architecture, where computing units execute ‘almost\
 nperiodically’, by adding a thin layer of middleware that facilitates\
 nthe implementation of synchronous applications.\n\nWe show how the depl
 oyment of a synchronous application on a\nquasi-periodic architecture ca
 n be modeled using a synchronous\nformalism. Then we detail two protocol
 s, Back-Pressure LTTA,\nreminiscent of elastic circuits, and Time-Based 
 LTTA, based on\nwaiting. Compared to previous work, we present controlle
 r models that\ncan be compiled for execution and a new version of the Ti
 me-Based\nprotocol that neither requires broadcast communication nor imp
 oses\nglobal synchronization. We also compare the LTTA approach with\nar
 chitectures based on clock synchronization.\n\nBased on an [EMSOFT 2015]
 (http://www.emsoft.org) presentation.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150925T151700
DTEND;TZID=Europe/Paris:20150925T173000
DTSTAMP;TZID=Europe/Paris:20150925T151700
UID:2015-09-25_Baghdadi
LOCATION:salle Cavaillès; 45 rue d'Ulm; ENS; Paris 5e
SEQUENCE:0
STATUS:CONFIRMED
SUMMARY:Riyadh Baghadi: Improving Tiling, Reducing Compilation Time, and
  Extending the Scope of Polyhedral Compilation
URL:http://parkas.di.ens.fr/seminars.html#2015-09-25_Baghdadi
DESCRIPTION:PhD thesis defense.\n\nWe are interested in enabling compile
 rs to automatically optimize and\nparallelize code. The polyhedral frame
 work is showing promising\nresults in this area. In this thesis, we addr
 ess three limitations in\nthe polyhedral framework and we present a prac
 tical solution to each\none of these limitations. First, we address the 
 problem of tiling code\nthat has false dependences. Compilers cannot til
 e such code without\nprivatization or expansion. To avoid this problem, 
 we propose a new\nrelaxed permutability criterion that allows a compiler
  to ignore false\ndependences between iteration-private live ranges and 
 thus enables the\ncompiler to tile the loops without privatization or ex
 pansion. Second,\nwe address the problem of compilation time. To reduce 
 the long\ncompilation time of large programs, we introduce a technique t
 hat we\ncall statement clustering and in which the original representati
 on of\nthe program is transformed into a new program representation (whe
 re\neach group of statements is represented as a macro-statement). The n
 ew\nrepresentation of the program can be optimized faster than the\norig
 inal representation. The third limitation is related to the\nability of 
 compilers to automatically parallelize irregular code and\nto generate e
 fficient code when information is missing to the\ncompiler. To address t
 his limitation, we introduce PENCIL, an\nintermediate language for DSL c
 ompilers and for accelerator\nprogramming. PENCIL is a subset of the C99
  language carefully designed\nto capture static properties essential to 
 enable more precise data\ndependence analysis. It provides also a set of
  language constructs\nthat enable parallelizing compilers to generate mo
 re efficient\ncode. The use of PENCIL would enable the compiler to gener
 ate\noptimized code that is quite difficult to generate otherwise.\n\nTh
 e members of the thesis committee are:\n\n* Stef Graillat, Professor, Un
 iversity Pierre et Marie Curie (President)\n* Cédric Bastoul, Professor
 , University of Strasbourg (Rapporteur)\n* Paul H J Kelly, Professor, Im
 perial College London (Rapporteur)\n* J. Ramanujam, Professor, Louisiana
  State University (Examinateur)\n* Albert Cohen, Senior Research Scienti
 st, INRIA, France (Directeur de thèse)\n* Sven Verdoolaege, Associate R
 esearcher, Polly Labs and KU Leuven (Encadrant)
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150907T163000
DTEND;TZID=Europe/Paris:20150907T173000
DTSTAMP;TZID=Europe/Paris:20150907T163000
UID:2015-09-07_vonHanxleden
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Reinhard von Hanxleden: Code-Generation for Sequential Construct
 iveness
URL:http://parkas.di.ens.fr/seminars.html#2015-09-07_vonHanxleden
DESCRIPTION:The Sequentially Constructive Language (SCL) is a minimal sy
 nchronous\nlanguage that captures the essence of the Sequentially Constr
 uctive model of\ncomputation (SC MoC), a recently proposed extension of 
 the classical\nsynchronous model of computation. The SC MoC uses sequent
 ial scheduling\ninformation to increase the class of constructive (legal
 ) synchronous\nprograms. This should facilitate the adoption of synchron
 ous programming by\nusers familiar with sequential programming in C or J
 ava, thus simplifying\nthe design of concurrent reactive/embedded system
 s with deterministic\nbehavior.  In this presentation, I focus on how to
  compile SCL down to\ndata-flow equations, which ultimately can be synth
 esized to hardware or\nexecuted in software.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150904T130000
DTEND;TZID=Europe/Paris:20150904T140000
DTSTAMP;TZID=Europe/Paris:20150904T130000
UID:2015-09-04_Andreani
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Virgile Andreani: Distributed Simulation of Hybrid Systems
URL:http://parkas.di.ens.fr/seminars.html#2015-09-04_Andreani
DESCRIPTION:The task of modelling and simulating a complex physical syst
 em is often a\nchallenge to engineers and researchers since the applicat
 ions of interest\nroutinely involve several time-scales, multiple sub-sy
 stems strongly or\nloosely coupled, and components whose behaviours are 
 very distinct.  The\nsimulation of such systems is done in most software
  by a single numeric\nsolver, which is often an inelegant solution, comp
 ared to harvesting the\nresults of a herd of specialised solvers, certai
 nly more efficient in their\nrespective tasks than a general purpose sol
 ver.  This talk will explore a\nfew leads to help shepherd several solve
 rs on the same simulation. Emphasis\nwill be placed on the role of 0th-o
 rder value holders in the computation,\nand on the compilation of a dist
 ributed simulation.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150703T150000
DTEND;TZID=Europe/Paris:20150703T163000
DTSTAMP;TZID=Europe/Paris:20150703T150000
UID:2015-07-03_Gramoli
LOCATION:Amphi Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Vincent Gramoli: Contention: can theory meet practice?
URL:http://parkas.di.ens.fr/seminars.html#2015-07-03_Gramoli
DESCRIPTION:With the growing core count on chip multiprocessors, content
 ion has\nbecome an important factor of performance degradation. Yet, lit
 tle\nefforts have been devoted to understanding how it affects performan
 ce of\ndata structures. Some were devoted to introducing different defin
 itions\nof contention whereas others were devoted to the implementation 
 of\nefficient data structures with terrible complexity. In the first par
 t of\nthis talk, I motivate the mismatch between some complexity metrics
  and\nperformance measurements by presenting a technique to reduce conte
 ntion\nin logarithmic data structures. In the second part of this talk, 
 I show\nthat definitions of contention can be considered equivalent in s
 ome\ncontext and illustrate this with an efficient concurrent linked lis
 t.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150626T103000
DTEND;TZID=Europe/Paris:20150626T120000
DTSTAMP;TZID=Europe/Paris:20150626T103000
UID:2015-06-26_Sarkar
LOCATION:salle Jean Jaurès; 29 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Vivek Sarkar: Structured Parallel Programming Primitives and the
 ir use in Compilers, Runtimes and Debuggers for Parallel Systems
URL:http://parkas.di.ens.fr/seminars.html#2015-06-26_Sarkar
DESCRIPTION:[Séminaire du DI](http://www.di.ens.fr/SeminaireGeneral.htm
 l.fr#Vendredi_26_juin_2015_10h30_Vive).\n\nIn this talk, we claim that s
 tructured parallel programming greatly\nsimplifies the task of writing c
 orrect and efficient parallel programs,\nwhile also capturing the flexib
 ility of expressing asynchronous\ncomputations.  We support this claim b
 y introducing a family of structured\nparallel programming primitives de
 veloped in the\n[Habanero Extreme Scale Software Research project](http:
 //habanero.rice.edu)\nat Rice University, and discussing semantic guaran
 tees (e.g., deadlock freedom,\ndata race freedom, determinism, serial el
 ision) for different subsets of\nparallel programs that can be construct
 ed with these primitives.  We will then\nsummarize results for\n[compile
 r optimizations](http://dl.acm.org/citation.cfm?id=2450138),\n[runtime s
 ystems](http://link.springer.com/chapter/10.1007%2F978-3-662-44202-9_25)
 ,\n[repair](http://dl.acm.org/citation.cfm?id=2254127) and\n[datarace de
 tection](http://dl.acm.org/citation.cfm?id=2594335) for these\nsubsets. 
 If time permits, we will briefly discuss future directions for\ndata-dri
 ven repair and synthesis of parallel programs in the new\n[Pliny project
 ](http://pliny.rice.edu).\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150611T130000
DTEND;TZID=Europe/Paris:20150611T140000
DTSTAMP;TZID=Europe/Paris:20150611T130000
UID:2015-06-11_Zhang
LOCATION:salle R; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Zhen Zhang: Time Mixed-Critical, Multi-Core Embedded Systems Des
 ign, Modeling and Implementation
URL:http://parkas.di.ens.fr/seminars.html#2015-06-11_Zhang
DESCRIPTION:The cost efficient integration of different applications wit
 h different\nlevels of safety and security on a single computing platfor
 m has become a\nmajor industrial challenge. Such a platform would prefer
 ably be an\noff-the-shelf shared memory multicore processor. The perform
 ance\nrequirements of individual applications and components also push f
 or their\nparallelization. Focusing on the safety-critical domain, we wo
 rk on\nextending to multicore processors with the established modular de
 sign and\nimplementation methods used for synchronous applications. In t
 his talk, I\nwill describe our approach to the modular composition of sy
 nchronous\ncomponents with hard real-time constraints. Preserving time-p
 redictability\nis the most difficult barrier to the adoption of multicor
 es in\nsafety-critical systems. Our solution is compatible with off-the-
 shelf\nembedded shared-memory multiprocessors, introducing minor modific
 ations to\nthe syntax and semantics of Heptagon, a synchronous programmi
 ng dialect of\nLustre. It is demonstrated on an industrial use case from
  Alstom Transport,\ninvolving a time-triggered software stack designed o
 n top of Linux and\nbare-metal components running on a Xilinx Zynq multi
 core platform. Our\nsolution involves an original methodology for the de
 sign of\n"mixed-time-critical" applications. The safety levels and corre
 ctness by\nconstruction of synchronous designs is preserved. Performance
  and time\npredictability can be traded off against each other. This inv
 olves the\npartitioning of an application into modes of different time c
 riticality, and\nis supported by time-critical backup scenarios when bes
 t-effort components\nmiss their deadline. This work takes place in the c
 ontext of the EMC2\nproject.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150601T130000
DTEND;TZID=Europe/Paris:20150601T140000
DTSTAMP;TZID=Europe/Paris:20150601T130000
UID:2015-06-01_Baghdadi
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Riyadh Baghdadi: PENCIL: a Platform-Neutral Compute Intermediate
  Language for DSL Compilers and for Accelerator Programming
URL:http://parkas.di.ens.fr/seminars.html#2015-06-01_Baghdadi
DESCRIPTION:Programming accelerators such as GPUs with low-level APIs an
 d languages like\nOpenCL and CUDA is difficult, error prone, and not per
 formance-portable.\nAutomatic parallelization and domain specific langua
 ges (DSLs) have been\nproposed to hide this complexity and to regain som
 e performance portability.\nIn this presentation, I will present PENCIL 
 (Platform-Neutral Compute\nIntermediate Language) and present some detai
 ls about how it is compiled.\nPENCIL is a rigorously defined subset of G
 NU C99 with specific programming\nrules and few extensions. Adherence to
  this subset and the use of these\nextensions enable compilers to exploi
 t parallelism and to better optimize\ncode when targeting accelerators. 
 We intend PENCIL both as a portable\nlanguage to facilitate accelerator 
 programming, and as an intermediate\nlanguage for DSL compilers. We vali
 date the potential of PENCIL on a\nstate-of-the-art polyhedral compiler,
  extending the applicability of the\ncompiler to dynamic, data-dependent
  control flow and non-affine array\naccesses. We use the polyhedral comp
 iler to generate highly optimized\nOpenCL code for a set of standard ben
 chmark suites (Rodinia and SHOC),\nimage processing kernels, and for two
  DSL compilers: a linear algebra (BLAS)\nDSL compiler and a DSL for sign
 al processing radar applications (SpearDE).\nTo assess performance porta
 bility, we present experimental results on many\nGPU platforms: AMD Rade
 on HD 5670, Nvidia GTX470, and ARM Mali-T604 GPU.\n\nBased on a [PACT 20
 15](http://www.pactconf.org) presentation.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150427T130000
DTEND;TZID=Europe/Paris:20150427T140000
DTSTAMP;TZID=Europe/Paris:20150427T130000
UID:2015-04-27_KroahHartman
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Greg Kroah-Hartman: An Introduction to Greybus
URL:http://parkas.di.ens.fr/seminars.html#2015-04-27_KroahHartman
DESCRIPTION:Greybus is the name for a new application layer protocol on 
 top of Unipro\nthat controls the Ara Phone from Google.  This protocol t
 urns a phone into a\nmodular device, allowing any part of the system to 
 be hotplugged while the\nphone is running.  This talk will describe what
  this protocol is, why it was\ndesigned, and give the basics for how it 
 works.  It will discuss how this is\nimplemented in the Linux kernel, an
 d how it easily bridges existing hardware\nlike USB, I2C, GPIO and other
 s with little to no changes needed to existing\nkernel drivers.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150413T130000
DTEND;TZID=Europe/Paris:20150413T140000
DTSTAMP;TZID=Europe/Paris:20150413T130000
UID:2015-04-13_MinhLe
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Nhat Minh Lê: Kahn process networks in the world of task parall
 elism
URL:http://parkas.di.ens.fr/seminars.html#2015-04-13_MinhLe
DESCRIPTION:This talk presents libkpn, a high-performance runtime system
  for task\nparallel programming, based on Kahn process networks (KPNs). 
 Away from the\nusual perception of KPNs as a high-level programming mode
 l compiled into\ngeneral-purpose languages, we explore how KPNs can be u
 sed directly as\nconcurrency specifications to guide dynamic scheduling 
 in a runtime system.\nThrough a comparison with existing models, we expl
 ain how features of KPNs\ncan be taken advantage of to allow more logica
 l parallelism to be expressed,\nand to create an efficient implementatio
 n.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150407T130000
DTEND;TZID=Europe/Paris:20150407T140000
DTSTAMP;TZID=Europe/Paris:20150407T130000
UID:2015-04-07_Bondhugula
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Uday Bondhugula: High-performance compilation through Domain-Spe
 cific Languages: the case of Image Processing Pipelines
URL:http://parkas.di.ens.fr/seminars.html#2015-04-07_Bondhugula
DESCRIPTION:This talk addresses the well-known challenge involved in sim
 ultaneously\ndelivering high productivity and high parallel performance 
 on modern\nmulticore architectures—through the development of domain-s
 pecific languages\n(DSLs) and their optimizing code generators. It prese
 nts the domain of Image\nProcessing Pipelines as the motivating case by 
 presenting PolyMage, our DSL\nand its code generator for automatic and e
 ffective optimization of image\nprocessing pipelines. PolyMage takes an 
 image processing pipeline expressed\nin a high-level language (embedded 
 in Python) and generates an optimized\nC/C++ implementation of the pipel
 ine. We show how certain techniques\nincluding those based on the polyhe
 dral compiler framework need to be\nspecialized in order to provide sign
 ificant improvements in parallel\nperformance over existing approaches i
 ncluding manual, library-based, and\nthat of another state-of-the-art DS
 L (Halide). More information at\nhttp://mcl.csa.iisc.ernet.in/polymage.h
 tml. Experimental results on a modern\nmulticore system and a short demo
  will also be presented.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150324T130000
DTEND;TZID=Europe/Paris:20150324T140000
DTSTAMP;TZID=Europe/Paris:20150324T130000
UID:2015-03-24_Mendler
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Michael Mendler: Constructive Semantics of Instantaneous Reactio
 ns
URL:http://parkas.di.ens.fr/seminars.html#2015-03-24_Mendler
DESCRIPTION:The synchronous model of programming, which emerged in the 1
 980s and has led\nto the development of well-known languages such as Sta
 techarts, Esterel,\nSignal, and Lustre, has made the programming of conc
 urrent systems with\ndeterministic and bounded reaction a routine exerci
 se.  The synchronous\napproach draws its success from the fact that it i
 s founded on a simple and\nwell-understood mathematical model of computa
 tion, the Mealy automaton.\nHowever, the validity of this model is not f
 or free. It depends on the\nSynchrony Hypothesis according to which a sy
 stem is invariably faster than\nits environment. Yet, this raises a tang
 led compositionality problem. Since\na node is in the environment of eve
 ry other node, it follows that each node\nmust be faster than every othe
 r and hence faster than itself!\n\nThis talk presents some results towar
 ds solving this paradox, refining the\nclassical Mealy model by construc
 tive notions of input-output causality.\nSpecifically, we propose a game
 -theoretic interpretation of the constructive\nsemantics of step respons
 es for synchronous languages, providing a coherent\nsemantic framework e
 ncompassing both non-deterministic Statecharts (as per\nPnueli & Shalev)
  and deterministic Esterel. In particular, it is shown that\nEsterel ari
 ses from a finiteness condition on strategies whereas Statecharts\npermi
 ts infinite games. Beyond giving a novel and unifying account of these\n
 concrete languages the talk sketches a general theory for obtaining\ndif
 ferent notions of constructive responses in terms of winning conditions\
 nfor finite and infinite games and their characterisation as maximal\npo
 st-fixed points of functions in directed complete lattices of intensiona
 l\ntruth-values.\n\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20150309T140000
DTEND;TZID=Europe/Paris:20150309T153000
DTSTAMP;TZID=Europe/Paris:20150309T140000
UID:2015-03-09_Adve
LOCATION:salle U/V; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Vikram Adve: Automated Bug Diagnosis and Virtual Instruction Set
  Computing
URL:http://parkas.di.ens.fr/seminars.html#2015-03-09_Adve
DESCRIPTION:The presentation has two parts:\n\n              PART 1: AUT
 OMATED BUG DIAGNOSIS\n              PART 2: VIRTUAL INSTRUCTION SET COMP
 UTING\n\nI will present our work on two ongoing projects: (1) automated\
 ndiagnosis of software failures, and (2) the benefits of using rich\nvir
 tual instruction sets as a persistent representation of _all_\nsoftware.
   If time permits, I will discuss a mythical connection\nbetween the two
  projects.\n\nIn the first part of the talk, I will describe new insight
 s into\nanalyzing the root causes of software failures automatically.  W
 e use\ndynamically observed likely invariants to identify candidate loca
 tions\nfor the root cause of a failure, and then use novel static and dy
 namic\nanalyses to filter out false positives and to extract valuable\ni
 nformation relevant to understanding the failure.  Experimental\nresults
  show that we are able to narrow down the locations of root\ncauses to j
 ust a few (e.g., 2-10) program locations, even in large\nprograms, for n
 early all bugs we have tested.  We are now exploring how\nto automate th
 e process fully using dynamic symbolic execution, and how\nto apply thes
 e fault isolation techniques for diagnosis and triaging of\nsoftware fai
 lures in production software.\n\nNext, I will discuss a project on Virtu
 al Instruction Set Computing\n(VISC). Despite extensive advances in mana
 ged run-time systems and\ndynamic compilation, high performance applicat
 ions and security\nsensitive systems software are almost universally com
 piled and shipped as native machine code.  In the VISC project, we are e
 xploring the\nsecurity, reliability, and performance implications of shi
 pping *all*\nsuch software in virtual instruction set form.  We use the 
 LLVM bitcode\nlanguage as the shipping representation to enable advanced
  "lifelong"\nprogram analysis and transformation for such programs.  We 
 have shown\nthat shipping operating systems in LLVM form enables powerfu
 l security\nguarantees to be enforced using compiler techniques.  We are
  now\nexploring how the approach could be used to improve programmabilit
 y and\nportability for heterogeneous parallel systems, and to enable nov
 el\nperformance optimization techniques.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20141217T100000
DTEND;TZID=Europe/Paris:20141217T110000
DTSTAMP;TZID=Europe/Paris:20141217T100000
UID:2014-12-17_Janin
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:David Janin: Flux média tuilés polymorphes: une expérimentati
 on en Haskell
URL:http://parkas.di.ens.fr/seminars.html#2014-12-17_Janin
DESCRIPTION:De nombreux outils sont aujourd'hui disponibles pour l'analy
 se et la\nproduction temps réel de flux média temporisés&nbsp;: sons,
  vidéo, animations,\netc. Néanmoins, la coordination de ces outils, la
  synchronisation des flux\nqu'ils analysent et produisent, sur des éche
 lles de temps de valeurs et même\nde nature différentes, reste une aff
 aire délicate.\n\nLe modèle des Tiled Polymorphic Temporal Media (ou T
 PTM), qui combine en un\nmême formalisme le contenu media de ces flux e
 t leurs marqueurs de\nsynchronisations, vise à remédier à cela. Dans 
 le modèle, le produit de deux\nflux ainsi enrichi, paramétré par ces 
 marqueurs de synchronisations, est\ntout à la fois séquentiel et paral
 lèle : c’est un produit tuilé.\n\nEn théorie, la sémantique de ces
  flux tuilés peut être décrite dans la\nthéorie des monoïdes invers
 ifs. En pratique, nous avons réalisé, en Haskell,\nla première implé
 mentation réellement polymorphe et inversive de ces Tiled\nPolymorphic 
 Temporal Media. Notre implémentation permet en outre, via le\nmécanism
 e d’évaluation paresseuse d’Haskell, de distinguer simplement la\ns
 yntaxe de ces flux – un système d’équations tuilées – de leur s
 émantique\nopérationnelle – la résolution de ce système à la vol
 ée.\n\nNous montrerons aussi comment nos constructions se généralisen
 t simplement\naux tuiles infinies.\n\nCe travail a été partiellement r
 éalisé en collaboration avec Paul Hudak\n(Yale) et Théis Bazin (Stagi
 aire, ENS Cachan).
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140630T103000
DTEND;TZID=Europe/Paris:20140630T113000
DTSTAMP;TZID=Europe/Paris:20140630T103000
UID:2014-06-30_Tinelli
LOCATION:salle Jules Ferry; 29 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Cesare Tinelli: SMT-based Unbounded Model Checking with IC3 and 
 Approximate Quantifier Elimination
URL:http://parkas.di.ens.fr/seminars.html#2014-06-30_Tinelli
DESCRIPTION:The IC3 procedure by A. Bradley is a recent model checking p
 rocedure for proving safety properties of finite-state systems that has 
 shown to be quite effective in practice. This talk presents an SMT-based
  version of IC3 that works with both finite- and infinite-state systems.
  A distinguishing feature of our approach is the use of approximate quan
 tifier elimination to generalize counterexamples. We provide experimenta
 l evidence that for linear integer arithmetic our method is superior in 
 practice to full-blown quantifier elimination, and that our IC3 implemen
 tation is competitive with a state-of-the-art k-induction model checker 
 for infinite-state systems. Our experiments also show that IC3 and k-ind
 uction have complementary strengths and so can be combined advantageousl
 y in a multi-engine parallel checker.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140623T100000
DTEND;TZID=Europe/Paris:20140623T110000
DTSTAMP;TZID=Europe/Paris:20140623T100000
UID:2014-06-23_Tinelli
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Cesare Tinelli: SMT-based Model Checking
URL:http://parkas.di.ens.fr/seminars.html#2014-06-23_Tinelli
DESCRIPTION:The field of model checking owes much of its great success a
 nd impact to the use of symbolic techniques to reason efficiently about 
 functional properties of hardware or software systems. Traditionally, th
 ese techniques have relied on propositional encodings of transition syst
 ems and on propositional reasoning engines such as binary decision diagr
 ams and SAT solvers. More recently, a number of these techniques have be
 en adapted, and new ones have been devised, based instead on encodings i
 nto fragments of first-order logic supported by Satisfiability Modulo Th
 eories (SMT) solvers. These are highly efficient solvers specialized on 
 checking the satisfiability of formulas in certain logical theories such
  as the theory of linear arithmetic, bit-vectors, arrays, algebraic data
  types, and so on.\nSMT-based model checking methods blur the line betwe
 en traditional (propositional) model checking and traditional (first or 
 higher order) deductive verification. More crucially, they combine the b
 est features of both by offering the scalability and scope of deductive 
 verification while maintaining comparable levels of automations as propo
 sitional model checking.\nThis talk will briefly introduce SMT and then 
 give an overview of SMT-based model checking, focusing on a number of no
 table approaches and techniques. 
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140526T103000
DTEND;TZID=Europe/Paris:20140526T120000
DTSTAMP;TZID=Europe/Paris:20140526T103000
UID:2014-05-26_Pessaux
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:François Pessaux: The FoCaLiZe language: mixing program and pro
 ofs
URL:http://parkas.di.ens.fr/seminars.html#2014-05-26_Pessaux
DESCRIPTION:FoCaLiZe is a programming language allowing to state in a sa
 me framework\nalgorithms (programming aspects), properties (logical aspe
 cts) that these\nalgorithms must satisfy and proofs these latter hold. I
 t provides high-level\nconstructs to ease development structuring and re
 use (modularity,\ninheritance, late-binding, parameterization) and a pro
 of language allowing\nto write proofs in a hierarchical way, using a nat
 ural deduction style, which\nrely on the Zenon automated theorem prover 
 to discharge goals ... and the\nburden of the user. The core programming
  language is a pure functional\nlanguage while properties are stated a f
 irst-order logic formulae.\nA FoCaLiZe development is compiled in two ta
 rget languages: one OCaml source\ncode leading to an executable (or obje
 ct file) and one Coq source code\ncontaining the complete model of the d
 evelopment (i.e. definitions, properties\nand proofs) that will be ultim
 ately checked by Coq as assessment. A crucial\ncare in this process is t
 o avoid any error from the target languages being\nreturned to the user:
  a program accepted by the FoCaLiZe compiler must be\naccepted by both O
 Caml and Coq. To increase confidence in "what is ran is\nwhat is proved"
  despite two target languages, the compiler has to use a\ncode generatio
 n model identical and traceable for both of them.\n\nIn this presentatio
 n we will introduce the motivations, design and\nfeatures choices that i
 mpacted the language semantics. The presentation\nof the language featur
 es and the development style will also be addressed\non the basis of exa
 mples, trying to illustrate advantages (and disavantages)\nof such a sys
 tem compared to other existing formal proofs systems.\n\n[Slides](slides
 /2014-05-26_Pessaux.pdf)
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140429T103000
DTEND;TZID=Europe/Paris:20140429T120000
DTSTAMP;TZID=Europe/Paris:20140429T103000
UID:2014-04-29_Schneider
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Sigurd Schneider: Translating In and Out of a Functional Interme
 diate Language
URL:http://parkas.di.ens.fr/seminars.html#2014-04-29_Schneider
DESCRIPTION:A functional intermediate language is a simple and effective
 \nformalization of static single assignment (SSA) for the purpose of\nve
 rified compilation of an imperative language. Two translations are of\np
 articular importance:\nTranslating from the imperative source language (
 e.g. C) to the\nfunctional language, and translating from the functional
  intermediate\nlanguage to an imperative target language (e.g. assembly)
 .\n\nThis talk discusses the above translations in the context of the\ni
 ntermediate language IL.\nIL comes with an imperative and a functional i
 nterpretation.\nIL/I (imperative interpretation) is a register transfer 
 language close\nto assembly.\nIL/F (functional interpretation) is a firs
 t-order functional language\nwith a tail-call restriction.\nWe devise th
 e decidable notion of coherence to identify programs on\nwhich the seman
 tics of IL/I and IL/F coincide.\nTranslations between the interpretation
 s are obtained from\nequivalence-preserving translations to the coherent
  fragment.\nThe translation from IL/I to IL/F corresponds to SSA constru
 ction.\nThe translation from IL/F to IL/I corresponds to SSA deconstruct
 ion and\ninvolves register assignment.\n\nThe translations are implement
 ed and proven correct using the proof\nassistant Coq. Extraction yields 
 translation-validated implementations\nof SSA construction and deconstru
 ction.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140418T103000
DTEND;TZID=Europe/Paris:20140418T120000
DTSTAMP;TZID=Europe/Paris:20140418T103000
UID:2014-04-18_Ding
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Chen Ding: Program Interaction in Shared Cache: Theory and Appli
 cations
URL:http://parkas.di.ens.fr/seminars.html#2014-04-18_Ding
DESCRIPTION:On modern multicore systems, the interaction between co-run 
 programs\nlargely depends on cache sharing, and cache sharing depends on
  the\nlocality, i.e. the active data usage, in co-run programs. This tal
 k\nintroduces a newly developed locality theory based on a concept calle
 d\nthe footprint. The theory shows the composability of footprint and th
 e\nconversion between footprint and other locality metrics. It enables\n
 accurate characterization and analysis of the dynamics of cache sharing.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140415T103000
DTEND;TZID=Europe/Paris:20140415T120000
DTSTAMP;TZID=Europe/Paris:20140415T103000
UID:2014-04-15_KrishnaRamanathan
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Murali Krishna Ramanathan: Multithreaded Test Synthesis for Dead
 lock Detection
URL:http://parkas.di.ens.fr/seminars.html#2014-04-15_KrishnaRamanathan
DESCRIPTION:Designing and implementing thread-safe multithreaded librari
 es can be a\ndaunting task as developers of these libraries need to ensu
 re that their\nimplementations are free from concurrency bugs including 
 deadlocks. The\nusual practice involves employing software testing and/o
 r dynamic\nanalysis to detect deadlocks. Their effectiveness is dependen
 t on\nwell-designed multithreaded test cases. Unsurprisingly, developing
 \nmultithreaded tests is easily an order of magnitude harder than\ndevel
 oping single threaded tests for obvious reasons.\n\nIn this talk, we wil
 l address the problem of automatically synthesizing\nmultithreaded tests
  that can induce deadlocks. The key insight to our\napproach is that a s
 ubset of the properties observed when a deadlock\nmanifests in a concurr
 ent execution can also be observed in a single\nthreaded execution. We d
 esign a novel, automatic, scalable and directed\napproach that identifie
 s these properties and synthesizes a\nmultithreaded test that realizes t
 hese properties simultaneously\nrevealing a potential deadlock. The inpu
 t to our approach is only the\nlibrary implementation under consideratio
 n and the output is a set of\ndeadlock revealing multithreaded tests. We
  will present the results of\nour analysis on synthesizing multithreaded
  tests for Java libraries. We\nfind 35 real deadlocks in thread safe cla
 sses in COLT, a popular high\nperformance scientific computing library.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140331T103000
DTEND;TZID=Europe/Paris:20140331T120000
DTSTAMP;TZID=Europe/Paris:20140331T103000
UID:2014-03-31_Oz
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Işıl Öz: Portable and Predictable Performance of Task-Based P
 arallel Applications
URL:http://parkas.di.ens.fr/seminars.html#2014-03-31_Oz
DESCRIPTION:Multicore systems yield high performance by the execution of
  multiple concurrent software processes in the system in a power and are
 a efficient way. While multicore systems are promising architectures for
  higher performance, the soft error reliability of these systems becomes
  a major concern due to smaller transistor sizes and low power operating
  modes.\n\nMy talk will include work during my Phd and recent work, rela
 ted to reliability and performance analysis of multicore systems.\n\nI a
 m currently working on ARTEMIS PaPP project. PaPP (Portable and Predicta
 ble Performance on Heterogeneous Embedded Manycores) aims to achieve pre
 dictable performance portability of software running on different parall
 el platforms. We focus on performance analysis modelling for task-based 
 parallel applications within multicore systems. Our modelling targets to
  find out minimal resources which satisfy performance requirements of an
  application and to develop task scheduling strategies as an input to ru
 n-time for better resource management and performance optimization.\n\nI
 n my PhD study, I was working on reliability analysis of multicore syste
 ms. I propose Thread Vulnerability Factor metric, to quantify vulnerabil
 ity of thread and to qualify the relative vulnerability of parallel appl
 ications to soft errors, and utilize the metric for performance-vulnerab
 ility analysis of parallel programs, reliability-aware core partitioning
  schemes for multicore architectures, and critical thread identification
  for redundant execution in a partial fault tolerance method. 
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140324T103000
DTEND;TZID=Europe/Paris:20140324T120000
DTSTAMP;TZID=Europe/Paris:20140324T103000
UID:2014-03-24_Balabonski
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Thibaut Balabonski: Data-race freedom by typing in Mezzo
URL:http://parkas.di.ens.fr/seminars.html#2014-03-24_Balabonski
DESCRIPTION:Mezzo is a typed programming language in the ML family whose
  static\ndiscipline controls aliasing and ownership. This rules out cert
 ain\nmistakes, including representation exposure and data races, and ope
 ns up\nnew opportunities, such as gradual initialization or (more genera
 lly,\nand somewhat speculatively) the definition and enforcement of obje
 ct\nprotocols.\n\nIn this talk, I will explain the basic design of Mezzo
  on examples, and\nshow how its type system gives a simple way of tracki
 ng ownership of\nfragments of shared memory between concurrent threads. 
 Beyond the usual\nclaim that "well-typed programs do not go wrong", we g
 uarantee that\nwell-typed Mezzo programs have no data-races.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20140213T103000
DTEND;TZID=Europe/Paris:20140213T120000
DTSTAMP;TZID=Europe/Paris:20140213T103000
UID:2014-02-13_Bhati
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Khurram Bhati: Predictable Execution of Task-Based Applications 
 on Multicore Systems
URL:http://parkas.di.ens.fr/seminars.html#2014-02-13_Bhati
DESCRIPTION:The presentation will have two parts. In the first part, we 
 will present\nan on-going research project to provide a run-time system 
 with\n"guidelines", using task graph properties, and a static analysis p
 hase\nto prioritize certain tasks of a given application over the others
 . The\norder in which tasks of an application task graph are considered 
 has a\nsignificant influence on the resulting schedule length. Gauging t
 he\nimportance of the tasks with a priority scheme is therefore a\nfunda
 mental part of scheduling schemes. We have used the concept of\npaths an
 d path lengths to gauge the importance of tasks in an offline\nstatic an
 alysis phase and provide guidelines to the run-time system for\npriority
  assignment.\n\nIn the second part of my presentation, we will present e
 arlier research\nresults that focuses on power/energy efficient real-tim
 e scheduling. We\nwill discuss at least one such technique to elaborate 
 the concept.
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20131004T103000
DTEND;TZID=Europe/Paris:20131004T120000
DTSTAMP;TZID=Europe/Paris:20131004T103000
UID:2013-10-04_LeeHung
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Prof. Jenq Kuen Lee and Dr. Ming-Yu Hung: Probabilistic Pointer 
 analysis in SSA Form and its Applications
URL:http://parkas.di.ens.fr/seminars.html#2013-10-04_LeeHung
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130919T140000
DTEND;TZID=Europe/Paris:20130919T150000
DTSTAMP;TZID=Europe/Paris:20130919T140000
UID:2013-09-19_Bhaskaracharya
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Somashekaracharya Bhaskaracharya: PolyGLoT - A Polyhedral Loop T
 ransformation Framework for a Graphical Dataflow Language
URL:http://parkas.di.ens.fr/seminars.html#2013-09-19_Bhaskaracharya
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130719T133000
DTEND;TZID=Europe/Paris:20130719T143000
DTSTAMP;TZID=Europe/Paris:20130719T133000
UID:2013-07-19_Rahli
LOCATION:salle R; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Vincent Rahli: EventML
URL:http://parkas.di.ens.fr/seminars.html#2013-07-19_Rahli
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130613T111500
DTEND;TZID=Europe/Paris:20130613T121500
DTSTAMP;TZID=Europe/Paris:20130613T111500
UID:2013-06-13_Sheeran
LOCATION:Salle Dussane; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Mary Sheeran: Obsidian: generating GPU kernels from Haskell
URL:http://parkas.di.ens.fr/seminars.html#2013-06-13_Sheeran
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130610T100000
DTEND;TZID=Europe/Paris:20130610T110000
DTSTAMP;TZID=Europe/Paris:20130610T100000
UID:2013-06-10_Govindarajan
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:R. Govindarajan: Compiling for Heterogeneous Multi-Core Architec
 tures with GPUs
URL:http://parkas.di.ens.fr/seminars.html#2013-06-10_Govindarajan
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130603T100000
DTEND;TZID=Europe/Paris:20130603T110000
DTSTAMP;TZID=Europe/Paris:20130603T100000
UID:2013-06-03_Hughes
LOCATION:salle U/V; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:John Hughes: Property-based testing with QuickCheck
URL:http://parkas.di.ens.fr/seminars.html#2013-06-03_Hughes
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130527T103000
DTEND;TZID=Europe/Paris:20130527T113000
DTSTAMP;TZID=Europe/Paris:20130527T103000
UID:2013-05-27_Chargueraud
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Arthur Charguéraud: Verification of Concurrent Programs Targeti
 ng the x86-TSO Weak Memory Model
URL:http://parkas.di.ens.fr/seminars.html#2013-05-27_Chargueraud
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130424T140000
DTEND;TZID=Europe/Paris:20130424T150000
DTSTAMP;TZID=Europe/Paris:20130424T140000
UID:2013-04-24_Keryell
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Ronan Keryell: SMECC: compiling the SME-C language for heterogen
 eous computing
URL:http://parkas.di.ens.fr/seminars.html#2013-04-24_Keryell
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130114T103000
DTEND;TZID=Europe/Paris:20130114T113000
DTSTAMP;TZID=Europe/Paris:20130114T103000
UID:2013-01-14_Grosser
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Tobias Grosser: Geometric time tiling of stencil computations
URL:http://parkas.di.ens.fr/seminars.html#2013-01-14_Grosser
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20130107T103000
DTEND;TZID=Europe/Paris:20130107T113000
DTSTAMP;TZID=Europe/Paris:20130107T103000
UID:2013-01-07_Sun
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Wei-Tsun Sun: The DynamicGALS approach to designing dynamic reac
 tive systems
URL:http://parkas.di.ens.fr/seminars.html#2013-01-07_Sun
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20121217T103000
DTEND;TZID=Europe/Paris:20121217T113000
DTSTAMP;TZID=Europe/Paris:20121217T103000
UID:2012-12-17_Serpette
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Bernard Serpette: Une définition CPS d'Esterel
URL:http://parkas.di.ens.fr/seminars.html#2012-12-17_Serpette
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20121105T103000
DTEND;TZID=Europe/Paris:20121105T113000
DTSTAMP;TZID=Europe/Paris:20121105T103000
UID:2012-11-05_Bagnol
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Marc Bagnol: Synchronous Machines: a Traced Category
URL:http://parkas.di.ens.fr/seminars.html#2012-11-05_Bagnol
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120907T110000
DTEND;TZID=Europe/Paris:20120907T120000
DTSTAMP;TZID=Europe/Paris:20120907T110000
UID:2012-09-07_Inoue
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jun Inoue: High-Level Programming That Works
URL:http://parkas.di.ens.fr/seminars.html#2012-09-07_Inoue
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120724T103000
DTEND;TZID=Europe/Paris:20120724T113000
DTSTAMP;TZID=Europe/Paris:20120724T103000
UID:2012-07-24_Cong
LOCATION:Amphi Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jason Cong: High-Level Synthesis Revisited: Progress and Applica
 tions
URL:http://parkas.di.ens.fr/seminars.html#2012-07-24_Cong
DESCRIPTION:[Slides](slides/2012-07-24_Cong.pdf).\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120626T103000
DTEND;TZID=Europe/Paris:20120626T113000
DTSTAMP;TZID=Europe/Paris:20120626T103000
UID:2012-06-26_Edwards
LOCATION:salle B14; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Stephen A. Edwards: From Recursive Functions to Real FPGAs
URL:http://parkas.di.ens.fr/seminars.html#2012-06-26_Edwards
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120523T140000
DTEND;TZID=Europe/Paris:20120523T150000
DTSTAMP;TZID=Europe/Paris:20120523T140000
UID:2012-05-23_Guatto
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Adrien Guatto: Code generation for Lucy-n: Issues and Perspectiv
 es
URL:http://parkas.di.ens.fr/seminars.html#2012-05-23_Guatto
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120419T103000
DTEND;TZID=Europe/Paris:20120419T113000
DTSTAMP;TZID=Europe/Paris:20120419T103000
UID:2012-04-19_DavidDelchini
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Vincent David et Hugo Delchini: Systèmes temps réel embarqués
  déterministes et sûrs de fonctionnement – OASIS & PharOS
URL:http://parkas.di.ens.fr/seminars.html#2012-04-19_DavidDelchini
DESCRIPTION:Cohabitation PharOS/EmbeddedC dans une application de contr
 ôle/commande de\nmoteur électrique pour du steer-by-wire avec retour d
 'effort Démonstration.\n
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120319T103000
DTEND;TZID=Europe/Paris:20120319T113000
DTSTAMP;TZID=Europe/Paris:20120319T103000
UID:2012-03-19_Chapoutot
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY: Alexandre Chapoutot : Vers un moteur de simulation ensembliste 
 de modèles Simulink
URL:http://parkas.di.ens.fr/seminars.html#2012-03-19_Chapoutot
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120305T103000
DTEND;TZID=Europe/Paris:20120305T113000
DTSTAMP;TZID=Europe/Paris:20120305T103000
UID:2012-03-05_Kerneis
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY: Gabriel Kerneis : From threads to events through classical prog
 ram transformations
URL:http://parkas.di.ens.fr/seminars.html#2012-03-05_Kerneis
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120220T103000
DTEND;TZID=Europe/Paris:20120220T113000
DTSTAMP;TZID=Europe/Paris:20120220T103000
UID:2012-02-20_Delaval
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY: Gwenaël Delaval : Musical programming with Lucid Synchrone
URL:http://parkas.di.ens.fr/seminars.html#2012-02-20_Delaval
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120213T103000
DTEND;TZID=Europe/Paris:20120213T113000
DTSTAMP;TZID=Europe/Paris:20120213T103000
UID:2012-02-13_Conchon
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Sylvain Conchon: Cubicle: A Parallel SMT-based Model Checker for
  Parameterized Systems
URL:http://parkas.di.ens.fr/seminars.html#2012-02-13_Conchon
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120130T103000
DTEND;TZID=Europe/Paris:20120130T113000
DTSTAMP;TZID=Europe/Paris:20120130T103000
UID:2012-01-30_Bouillard
LOCATION:salle B14; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Anne Bouillard: Algorithmic Issues in Network Calculus
URL:http://parkas.di.ens.fr/seminars.html#2012-01-30_Bouillard
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20120116T133000
DTEND;TZID=Europe/Paris:20120116T143000
DTSTAMP;TZID=Europe/Paris:20120116T133000
UID:2012-01-16_Filliatre
LOCATION:salle U/V; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jean-Christophe Filliâtre: Deductive Program Verification with 
 Why3
URL:http://parkas.di.ens.fr/seminars.html#2012-01-16_Filliatre
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20111205T103000
DTEND;TZID=Europe/Paris:20111205T113000
DTSTAMP;TZID=Europe/Paris:20111205T103000
UID:2011-12-05_Plaice
LOCATION:salle B14; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY: John Plaice : TransLucid
URL:http://parkas.di.ens.fr/seminars.html#2011-12-05_Plaice
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20111102T103000
DTEND;TZID=Europe/Paris:20111102T113000
DTSTAMP;TZID=Europe/Paris:20111102T103000
UID:2011-11-02_Nicolau
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Alex Nicolau: Variability, Accuracy, and Performance evaluation
URL:http://parkas.di.ens.fr/seminars.html#2011-11-02_Nicolau
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110919T103000
DTEND;TZID=Europe/Paris:20110919T113000
DTSTAMP;TZID=Europe/Paris:20110919T103000
UID:2011-09-19_Ishii
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Daisuke Ishii: An Execution Algorithm for a Hybrid Modeling Lang
 uage HydLa
URL:http://parkas.di.ens.fr/seminars.html#2011-09-19_Ishii
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110819T103000
DTEND;TZID=Europe/Paris:20110819T113000
DTSTAMP;TZID=Europe/Paris:20110819T103000
UID:2011-08-19_Gammie
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Peter Gammie: Verified Synthesis of Knowledge-Based Programs in 
 Finite Synchronous Environments
URL:http://parkas.di.ens.fr/seminars.html#2011-08-19_Gammie
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110720T100000
DTEND;TZID=Europe/Paris:20110720T113000
DTSTAMP;TZID=Europe/Paris:20110720T100000
UID:2011-07-20_Giavitto
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jean-Louis Giavitto: MGS : construire des représentations spati
 ales de processus musicaux
URL:http://parkas.di.ens.fr/seminars.html#2011-07-20_Giavitto
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110720T100000
DTEND;TZID=Europe/Paris:20110720T113000
DTSTAMP;TZID=Europe/Paris:20110720T100000
UID:2011-07-20_Echeveste
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:José Echeveste et Arshia Cont: Antescofo : formalisation des re
 lations temporelles entre une partition et une performance musicale
URL:http://parkas.di.ens.fr/seminars.html#2011-07-20_Echeveste
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110720T100000
DTEND;TZID=Europe/Paris:20110720T113000
DTSTAMP;TZID=Europe/Paris:20110720T100000
UID:2011-07-20_Bresson
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jean Bresson: OpenMusic : programmation visuelle et composition 
 assistée par ordinateur
URL:http://parkas.di.ens.fr/seminars.html#2011-07-20_Bresson
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110711T103000
DTEND;TZID=Europe/Paris:20110711T113000
DTSTAMP;TZID=Europe/Paris:20110711T103000
UID:2011-07-11_Encrenaz
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Emmanuelle Encrenaz: A Symbolic Model-Checking Framework for Tra
 nsient Fault Robustness Classification and Quantification
URL:http://parkas.di.ens.fr/seminars.html#2011-07-11_Encrenaz
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110630T110000
DTEND;TZID=Europe/Paris:20110630T123000
DTSTAMP;TZID=Europe/Paris:20110630T110000
UID:2011-06-30_Darte
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Alain Darte: Program Analysis and Source-Level Communication Opt
 imizations for High-Level Synthesis
URL:http://parkas.di.ens.fr/seminars.html#2011-06-30_Darte
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110630T100000
DTEND;TZID=Europe/Paris:20110630T110000
DTSTAMP;TZID=Europe/Paris:20110630T100000
UID:2011-06-30_Carle
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Thomas Carle: Throughput optimization by software pipelining of 
 conditional reservation tables
URL:http://parkas.di.ens.fr/seminars.html#2011-06-30_Carle
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110614T150000
DTEND;TZID=Europe/Paris:20110614T160000
DTSTAMP;TZID=Europe/Paris:20110614T150000
UID:2011-06-14_Vitek
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Jan Vitek: Virtualizing Real-time Embedded Systems with Java
URL:http://parkas.di.ens.fr/seminars.html#2011-06-14_Vitek
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110606T110000
DTEND;TZID=Europe/Paris:20110606T120000
DTSTAMP;TZID=Europe/Paris:20110606T110000
UID:2011-06-06_MunierKordon
LOCATION:salle U/V; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Alix Munier-Kordon: Etude de la minimisation de la surface des m
 émoires-buffers pour une application modélisée par un graphe « Synch
 ronous Data-Flow »
URL:http://parkas.di.ens.fr/seminars.html#2011-06-06_MunierKordon
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110523T103000
DTEND;TZID=Europe/Paris:20110523T113000
DTSTAMP;TZID=Europe/Paris:20110523T103000
UID:2011-05-23_Lowinger
LOCATION:salle U/V; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Hélène Lowinger: Présentation des outils de l'information sci
 entifique et technique de l'INRIA
URL:http://parkas.di.ens.fr/seminars.html#2011-05-23_Lowinger
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110513T103000
DTEND;TZID=Europe/Paris:20110513T120000
DTSTAMP;TZID=Europe/Paris:20110513T103000
UID:2011-05-13_Najjar
LOCATION:Salle W; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Prof. Walid Najjar: Performance, Productivity and Programmabilit
 y: The Coming of Age of FPGA Code Accelerators
URL:http://parkas.di.ens.fr/seminars.html#2011-05-13_Najjar
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110328T113000
DTEND;TZID=Europe/Paris:20110328T123000
DTSTAMP;TZID=Europe/Paris:20110328T113000
UID:2011-03-28_Upadrasta
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Ramakrishna Upadrasta: Potential and Challenges of Two-Variable-
 Per-Inequality Sub-Polyhedral Compilation
URL:http://parkas.di.ens.fr/seminars.html#2011-03-28_Upadrasta
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110328T103000
DTEND;TZID=Europe/Paris:20110328T113000
DTSTAMP;TZID=Europe/Paris:20110328T103000
UID:2011-03-28_Park
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Eunjung Park: Predictive Modeling in a Polyhedral Optimization S
 pace
URL:http://parkas.di.ens.fr/seminars.html#2011-03-28_Park
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110321T083000
DTEND;TZID=Europe/Paris:20110321T093000
DTSTAMP;TZID=Europe/Paris:20110321T083000
UID:2011-03-21_Li
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Feng Li: Advances in Parallel-stage Decoupled Software Pipelinin
 g
URL:http://parkas.di.ens.fr/seminars.html#2011-03-21_Li
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110307T103000
DTEND;TZID=Europe/Paris:20110307T113000
DTSTAMP;TZID=Europe/Paris:20110307T103000
UID:2011-03-07_Bourke
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Timothy Bourke: OCaml/Sundials
URL:http://parkas.di.ens.fr/seminars.html#2011-03-07_Bourke
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20110131T143000
DTEND;TZID=Europe/Paris:20110131T153000
DTSTAMP;TZID=Europe/Paris:20110131T143000
UID:2011-01-31_ZappaNardelli
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Francesco Zappa-Nardelli: Shared Memory: an Elusive Abstraction
URL:http://parkas.di.ens.fr/seminars.html#2011-01-31_ZappaNardelli
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20101213T103000
DTEND;TZID=Europe/Paris:20101213T113000
DTSTAMP;TZID=Europe/Paris:20101213T103000
UID:2010-12-13_Boudeville
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Olivier Boudeville: Présentation de SimDiasca (Simulation of Di
 screte Systems of All Scales)
URL:http://parkas.di.ens.fr/seminars.html#2010-12-13_Boudeville
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20101213T103000
DTEND;TZID=Europe/Paris:20101213T113000
DTSTAMP;TZID=Europe/Paris:20101213T103000
UID:2010-12-13_Pasteur
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Cédric Pasteur: Programming agents in ReactiveML
URL:http://parkas.di.ens.fr/seminars.html#2010-12-13_Pasteur
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20101124T133000
DTEND;TZID=Europe/Paris:20101124T143000
DTSTAMP;TZID=Europe/Paris:20101124T133000
UID:2010-11-24_Gerard
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Léonard Gérard: The basis of a bursty synchronous language, it
 s clock system and a causality analysis
URL:http://parkas.di.ens.fr/seminars.html#2010-11-24_Gerard
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20101115T103000
DTEND;TZID=Europe/Paris:20101115T113000
DTSTAMP;TZID=Europe/Paris:20101115T103000
UID:2010-11-15_MandelPlateau
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Louis Mandel et Florence Plateau: Typage d'horloges périodiques
  en Lucy-n
URL:http://parkas.di.ens.fr/seminars.html#2010-11-15_MandelPlateau
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20101011T150000
DTEND;TZID=Europe/Paris:20101011T160000
DTSTAMP;TZID=Europe/Paris:20101011T150000
UID:2010-10-11_Donaldson
LOCATION:salle S16; Aile Rataud; 45 rue d'Ulm; Paris 5e
SEQUENCE:1
STATUS:CONFIRMED
SUMMARY:Alastair F. Donaldson: An Induction-based Method for Complete Bo
 unded Model Checking of Programs
URL:http://parkas.di.ens.fr/seminars.html#2010-10-11_Donaldson
DESCRIPTION:
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR