BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Google Inc//Google Calendar 70.9054//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
DESCRIPTION:Analyse et conception de systèmes seminar of IRIF
NAME:Analyse et conception de systèmes
REFRESH-INTERVAL:PT4H
TIMEZONE-ID:Europe/Paris
X-WR-CALDESC:Analyse et conception de systèmes seminar of IRIF
X-WR-CALNAME:Analyse et conception de systèmes
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:Computing means and moments of occurrence counts: rule-based model
ing meets adaptive uniformization and finite state projection - Tobias Hei
ndel\, University of Copehagen
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160407T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160407T153000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:74
DESCRIPTION:The talk presents recent results on how to solve the general p
roblem of computing the time evolution of means and moments of ``occurence
counts'' in rule-based models\; computability is in the sense of Weihrauc
h. Roughly\, established techniques\, namely adaptive uniformization and
finite state projection\, can be reused -- provided that occurrence counts
(and their powers) are bounded by a polynomial in the ``size'' of the rul
e-based system and the ``size'' of the system does not explode. The most
interesting results can be obtained for context-free systems\, which can b
e thought of as branching processes equipped with structure\; for these sy
stems we have PTIME computability.\n\nAll results will be exemplified for
the case of string rewriting\, aiming for a widest possible audience of co
mputer scientists\, assuming only basic knowledge of continous time Markov
chains with countable state space. Computing the time evolution of mean
word counts in stochastic string rewriting is already highly non-trivial\,
even if it is the most basic example. The GEM OF THE TALK is the computa
tion of mean word counts for context-free grammars!
LOCATION:Salle UFR
END:VEVENT
BEGIN:VEVENT
SUMMARY:Towards the verification of file tree transformations - the Colis
project - Ralf Treinen\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160526T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160526T153000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:75
DESCRIPTION:This talk describes a recently started ANR project named Colis
\n(http://colis.irif.univ-paris-diderot.fr/)\, which has the goal of\ndeve
loping techniques and tools for the formal verification of shell\nscripts.
More specifically\, our goal is to verify the transformation\nof a file s
ystem tree described by so-called debian maintainer\nscripts. These script
s\, often written in the Posix shell language\, are\npart of the software
packages in the Debian GNU/Linux distribution.\n\nA possible example of a
program specification is absence of execution\nerror under certain initial
conditions. Automatic program verification\neven for this kind of specifi
cation is a challenging task. In case of\nDebian maintainer scripts we are
faced with even more challenging\nproperties like idempotency of scripts
(required by policy)\, or\ncommutation of scripts.\n\nThe project is still
in the beginning\, so there are no results yet to\npresent. However\, I w
ill explain why I think that the case of Debian\nmaintainer scripts is ver
y interesting for program verification : some\naspects of scripts (POSIX s
hell\, manipulation of a complex data\nstructure) make the problem very di
fficult\, while other aspects of the\nDebian case are likely to make the p
roblem easier than the task of\nverifying any arbitary shell script.
LOCATION:Salle 1008
END:VEVENT
BEGIN:VEVENT
SUMMARY:Analyse qualitative des réseaux de régulation génétiques - Eli
sabeth Remy\, Institut de Mathématiques de Luminy
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160623T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160623T153000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:84
DESCRIPTION:Les modèles d’interactions Booléens ont été introduits d
ans le contexte des réseaux de gènes par S. Kauffman dans la fin des ann
ées 60. On considère ici une variante\, les modèles logiques\, qui repo
sent sur un formalisme qualitatif avec mise à jour asynchrone des systèm
es dynamiques discrets associés (R. Thomas\, 1973). \nL’expression d'un
gène y est représentée par une variable discrète et l’évolution du
réseau est contrôlée par un système d'équations logiques. A partir d
e ce système peut être extrait un graphe de régulation : il s’agit d
’un graphe orienté signé\, dont les noeuds représentent les gènes\,
et les arcs les régulations entre gènes. On y distingue deux types de r
égulations : les activations (interactions positives) et les inhibitions
(interactions négatives). \nCes modèles génèrent des dynamiques de tai
lle exponentielle\, et nous faisons face à des problèmes d’explosion c
ombinatoire.\nAinsi\, nous cherchons à caractériser des propriétés de
la dynamique (attracteurs\, atteignabilité\,...) sans avoir à générer
le graphe de transition d’états\, qui représente l’ensemble des traj
ectoires possibles.\nUne méthode consiste à réduire le graphe\, et étu
dier la dynamique réduite. L’opération de réduction crée des modific
ations potentiellement importantes dans la dynamique\, il est donc nécess
aire de bien caractériser ses propriétés de (non-)conservation. Nous ve
rrons aussi comment identifier les attracteurs et quantifier leurs bassins
d’attraction à l’aide de méthodes de Monte-Carlo adaptées.\nEnfin\
, nous mettrons en valeur ces méthodes d'analyse à travers l’étude d
’un modèle concernant la tumorigénèse du cancer de vessie.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Building Graphical Choreographies From Communicating Machines: Pri
nciples and Applications - Julien Lange\, Imperial College
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161201T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161201T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:156
DESCRIPTION:Graphical choreographies\, or global graphs\, are general mult
iparty session specifications featuring expressive constructs such as fork
ing\, merging\, and joining for representing application-level protocols.
Global graphs can be directly translated into modelling notations such as
BPMN and UML. In the first part of the talk\, I will first present an algo
rithm whereby a global graph can be constructed from asynchronous interact
ions represented by communicating finite-state machines (CFSMs)\; and a so
und characterisation of a subset of safe CFSMs from which global graphs ca
n be constructed. In the second part\, I will outline a few recent applica
tions of this work to communicating timed automata and the Go programming
language.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Full-abstraction for Must Testing Preorders - Giovanni Bernardi\,
IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170518T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170518T153000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:236
DESCRIPTION:The client Must preorder relates tests (clients) instead of\np
rocesses (servers). The existing characterisation of this preorder\nis uns
atisfactory for it relies on the notion of usable clients which\, in turn\
,\nare defined using an existential quantification over the servers that e
nsure\nclient satisfaction.\nIn this talk we characterise the set of usabl
e clients for finite-branching LTSs\,\nand give a sound and complete deci
sion procedure for it.\nWe also provide a novel coinductive characterisati
on of the client preorder\,\nwhich we use to argue that the preorder is de
cidable\, thus proving a claim\nmade by Bernardi and Hennessy in 2013.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Who needs theorem provers when we have compilers? - Joachim Breitn
er\, University of Pennsylvania
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170502T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170502T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:243
DESCRIPTION:After decades of work on functional programming and on interac
tive\ntheorem proving\, a Haskell programmer who wants to include simple\n
equational proofs in his programs\, e.g. that some Monad laws hold\, is\ns
till most likely to simply do the derivation as comments in the file\,\nas
all the advanced powerful proving tools are inconvenient.\n\nBut one powe
rful tool capable of doing (some of) these proofs is\nhidden in plain sigh
t: GHC\, the Haskell compiler! Its optimization\nmachinery\, in particular
the simplifier\, can prove many simple\nequations all by himself\, simply
by compiling both sides and noting\nthat the result is the same. Furtherm
ore\, and crucially to make this\napproach applicable to more complicated
equations\, the compiler can be\ninstructed to do almost arbitrary symboli
c term rewritings by using\nRewrite Rules.\n\nIn this rather hands-on talk
I will show a small GHC plugin that I can\nuse to prove the monad laws fo
r a non-trivial functor. I am looking\nforward to a discussion of the meri
ts\, limits and capabilities of this\napproach.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:A simplicial complex model of dynamic epistemic logic for fault-to
lerant distributed computing - Eric Goubault\, LIX\, École Polytechnique
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170608T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170608T150000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:244
DESCRIPTION:The usual epistemic S5 model for multi-agent systems is a Krip
ke graph\, whose edges are labeled with the agents that do not distinguish
between two states. We propose to uncover the higher dimensional informat
ion implicit in the Kripke graph\, by using as a model its dual\, a chroma
tic simplicial complex. For each state of the Kripke model there is a face
t in the complex\, with one vertex per agent. If an edge (u\,v) is labeled
with a set of agents S\, the facets corresponding to u and v intersect in
a simplex consisting of one vertex for each agent of S. Then we use dynam
ic epistemic logic to study how the simplicial complex epistemic model cha
nges after the agents communicate with each other. We show that there are
topological invariants preserved from the initial epistemic complex to the
epistemic complex after an action model is applied\, that depend on how r
eliable the communication is. In turn these topological properties determi
ne the knowledge that the agents may gain after the communication happens.
\n\nWe choose distributed computing as a case study to work out in detail
the dynamic epistemic simplicial complex theory. The reason is that distri
buted computability has been studied using combinatorial topology\, where
the set of all possible executions in a\ndistributed system is represented
by a simplicial complex.\nWe establish a formal\, categorical equivalence
between Kripke models and simplicial complex epistemic models.\n\nIn one
direction\, the connection provides a dynamic epistemic logic semantics to
distributed computability\,\nopening the possibility of reasoning about k
nowledge change in distributed\ncomputing.\nIn the other direction\, the c
onnection allows to bring in the topological invariants known in distribut
ed computing\,\nto dynamic epistemic logic\, and in particular show that k
nowledge gained after an epistemic action model\nis intimately related to
higher dimensional topological properties.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Formal methods in action: typestate-oriented actor programming in
Scala-Akka - Silvia Crafa\, Università di Padova
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170529T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170529T150000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:265
DESCRIPTION:Typestate-oriented programming is an extension of the OO parad
igm in which objects are modelled not just in terms of interfaces but also
in terms of their usage protocols\, describing legal sequences of method
calls\, possibly depending on the object’s internal state. We argue that
the Actor Model allows typestate-OOP in an inherently distributed setting
\, whereby objects/actors can be accessed concurrently by several processe
s\, and local entities cooperate to carry out a communication protocol.\nI
n this talk we examine a “full stack development”: we skip through a
process calculus of actors equipped with a behavioural type system that al
lows to declare\, to statically check and to infer state-based protocols\,
and we see it in action on Scala Akka programs\, showing how far the stan
dard Scala compiler supports protocol checking and\ndiscussing current wor
k on compiler extension.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:The stochastic mechanics of graph rewriting via the rule algebra f
ramework - an introduction - Nicolas Behr\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171018T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171018T153000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:326
DESCRIPTION:Reporting on joint work with V. Danos and I. Garnier\, I will
present a novel formulation of graph rewriting that permits to phrase the
concept in a fashion akin to statistical physics. The key ingredient of th
is approach is the rule algebra framework\, in which rewriting rules are i
nterpreted as a type of diagrams endowed with a notion of sequential compo
sitions. The focus of this talk will be the stochastic mechanics applicati
ons: once an associative algebra of rewriting rules is available in the fo
rm of the rule algebras\, the full theory of continuous time Markov chains
is at ones disposal. A number of explicit examples for computing in this
formalism will be presented.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:The Spirit of Ghost Code - Leon Gondelman\, Institute for Computat
ion and Information Sciences (Radboud Univ.)\, Netherlands
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171128T133000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171128T143000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:364
DESCRIPTION:In the context of deductive program verification\, ghost code
is part of the program that is added for the purpose of specification. Gho
st code must not interfere with regular code\, in the sense that it can be
erased without any observable difference in the program outcome. In part
icular\, ghost data cannot participate in regular computations and ghost c
ode cannot mutate regular data or diverge. The idea exists in the folklore
since the early notion of auxiliary variables and is implemented in many
state-of-the-art program verification tools. However\, a rigorous definiti
on and treatment of ghost code is surprisingly subtle and few formalizatio
ns exist.\n\nIn this talk\, we describe a simple ML-style programming lang
uage with mutable state and ghost code. Non-interference is ensured by a
type system with effects\, which allows\, notably\, the same data types an
d functions to be used in both regular and ghost code. We define the proc
edure of ghost code erasure and we prove its safety using bisimulation. A
similar type system\, with numerous extensions which we briefly discuss\,
is implemented in the program verification environment Why3.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Informal introduction to integral probability metrics and generati
ve adversarial networks - Hongseok Yang\, University of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180207T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180207T150000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:446
DESCRIPTION:This is an informal whiteboard/blackboard presentation on gene
rative adversarial networks by a non-expert. I will explain integral proba
bility metrics and their use on training deep generative models\, widely k
nown as GAN (generative adversarial networks). My plan is to focus on two
well-known metrics for probability distributions\, Wasserstein distance an
d Maximum Mean Discrepancy. I will explain how their dual characterisation
s have been used in the adversarial training of deep generative models\, a
nd I will make superficial/speculative comparisons between these metrics.
My talk will be based on the following papers and the slides:\n\nReference
s:\nWasserstein GAN\nhttps://arxiv.org/abs/1701.07875\n\nGenerative Models
and Model Criticism via Optimized Maximum Mean Discrepancy\nhttps://arxiv
.org/abs/1611.04488\n\nMaximum Mean Discrepancy\nhttp://alex.smola.org/tea
ching/iconip2006/iconip_3.pdf
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:The "Hilbert Method" for Solving Transducer Equivalence Problems -
Adrien Boiret\, University of Warsaw
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180219T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180219T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:529
DESCRIPTION:Classical results from algebra\, such as Hilbert's Basis Theor
em and Hilbert’s Nullstellensatz\, have been used to decide equivalence
for some classes of transducers\, such as HDT0L (Honkala 2000) or more rec
ently deterministic tree-to-string transducers (Seidl\, Maneth\,\nKemper 2
015). In this talk\, we propose an abstraction of these methods. The goal
is to investigate the scope of the “Hilbert method” for transducer equ
ivalence that was described above.\n\nConsider an algebra A in the sense o
f universal algebra\, i.e. a set equipped with some operations. A grammar
over A is like a context-free grammar\, except that it generates a subset
of the algebra A\, and the rules use operations from the algebra A. The cl
assical context-free\ngrammars are the special case when the algebra A is
the free monoid with concatenation. Using the “Hilbert method” one ca
n decide certain properties of grammars over algebras that are fields or r
ings of polynomials over a field. The “Hilbert method” extends to gram
mars\nover certain well-behaved algebras that can be “coded” into fiel
ds or rings of polynomials. Finally\, for these well-behaved algebras\, on
e can also use the “Hilbert method” to decide the equivalence problem
for transducers (of a certain transducer model that uses registers)\nthat
input trees and output elements of the well-behaved algebra.\n\nIn the tal
k\, we give examples and non-examples of well-behaved algebras\, and discu
ss the decidability / undecidability results connected to them. In particu
lar:\n\n -We show that equivalence is decidable for transducers that input
(possibly ordered) trees and output unranked unordered trees. \n\n -We sh
ow that equivalence is undecidable for transducers that input words and ou
tput polynomials over the rational numbers with one variable (but are allo
wed to use composition of polynomials).\n\nJoint work with Mikołaj Bojań
czyk\, Janusz Schmude\, Radosław Piórkowski at Warsaw University.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:FreeSpec : Modular Verification of Systems using Effects and Effec
t Handlers in Coq - Thomas Letan\, Agence Nationale de la Sécurité des S
ystèmes d’Information & INRIA Rennes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180314T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180314T150000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:545
DESCRIPTION:Modern computing systems have grown in complexity\, and the at
tack surface has increased accordingly.\n\nEven though system components a
re generally carefully designed and even\nverified by different groups of
people\, the \\textit{composition} of these\ncomponents is often regarded
with less attention.\n\nThis paves the way for “architectural attacks”
\, a class of security\nvulnerabilities where the attacker is able to thre
aten the security of the\nsystem even if each of its component continues t
o act as expected.\n\nIn this article\, we introduce FreeSpec\, a Coq fram
ework built upon\nthe key idea that components can be modelled as programs
with\nalgebraic effects to be realized by other components.\n\nFreeSpec a
llows for the modular modelling of a complex system\, by\ndefining idealiz
ed components connected together\, and the modular\nverification of the pr
operties of their composition.\n\nIn doing so\, we propose a novel approac
h for the Coq proof assistant\nto reason about programs with effects in a
modular way.
LOCATION:Salle UFR
END:VEVENT
BEGIN:VEVENT
SUMMARY:Reactive Probabilistic Programming - Louis Mandel\, IBM Watson
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190107T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190107T113000
DTSTAMP;VALUE=DATE-TIME:20191207T110301Z
UID:677
DESCRIPTION:The idea of Probabilistic Programming is to use the expressive
ness of\nprogramming languages to build probabilistic models. To implement
this\nidea\, a common approach is to take a general purpose language and\
nextend it with (1) a function that allows to sample a value from a\ndistr
ibution\, (2) a function that allows to condition values of\nvariables in
a program via observations\, and (3) an inference\nprocedure that build a
distribution for a program using the two\nprevious constructs.\n\nFollowin
g this approach\, we propose to extends a reactive programming\nlanguage w
ith probabilistic constructs. This new language enables the\nmodeling of p
robabilistic reactive systems\, that is\, probabilistic\nmodels in constan
t interaction with their environment. Examples of\nsuch systems include ti
me-series prediction\, agent-based systems\, or\ninfrastructure self-tunin
g.\n\nTo demonstrate this approach\, we started from ReactiveML\, a reacti
ve\nextension of OCaml that supports parallel composition of processes\,\n
communication through signals\, preemption\, and suspension. We extend\nt
he language with classic probabilistic constructs (sample\, factor à\nla
WebPPL) and propose an inference scheme for reactive processes\,\nthat are
\, non-terminating functions.
LOCATION:Salle 3052
END:VEVENT
END:VCALENDAR