BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Google Inc//Google Calendar 70.9054//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
DESCRIPTION:Vérification seminar of IRIF
NAME:Vérification
REFRESH-INTERVAL:PT4H
TIMEZONE-ID:Europe/Paris
X-WR-CALDESC:Vérification seminar of IRIF
X-WR-CALNAME:Vérification
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:Low-level C code optimisations: are they valid? - Thibaut Balabons
ki\, LRI
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160530T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160530T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:78
DESCRIPTION:ubstantial research efforts have been devoted to tools for rea
soning about -and proving properties of- programs. A related concern is ma
king sure that compilers preserve the soundness of programs\, that is maki
ng sure that the compiled code respects the behavior of the source program
(see for instance the CompCert C compiler).\nThis talk is about an attemp
t at proving the soundness of some basic low-level transformations for con
current C programs. We will see some elements of the official semantics of
concurrency in C\, and I will relate how the focus of this work shifted f
rom proving the soundness of program transformations to patching the offic
ial semantics.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Abstraction-based Verification of Infinite-state Data-aware System
s - Francesco Belardinelli\, Université d'Evry
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160919T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160919T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:106
DESCRIPTION:Data-aware Systems (DaS) are a novel paradigm to model busines
s processes in Service-oriented Computing.\n\nDaS are best described in te
rms of interacting modules consisting of a data model and a lifecycle\, wh
ich account respectively for the relational structure of data and their ev
olution over time.\n\nHowever\, by considering data and processes as equal
ly relevant tenets of DaS\, the typical questions concerning their verific
ation are hardly amenable by current methodologies. For instance\, the pre
sence of data means that the number of states in DaS is infinite in genera
l.\n\nIn this talk we present recent advances in the verification of DaS.
We introduce agent-based abstraction techniques to model check DaS against
specifications expressed in temporal and strategy logics. Further\, we il
lustrate how DaS can be useful to model game-theoretic scenarios as well.
Specifically\, we provide an analysis of English (ascending bid) auctions
through DaS.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Polynomial invariants by linear algebra - Steven de Oliveira\, CEA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161010T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161010T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:108
DESCRIPTION:One of the main issue in formal verification is the analysis o
f loops\,\nconsidered as a major research problem since the 70s. Program\n
verification based on Floyd-Hoare's inductive assertion and CEGAR-like\nte
chniques for model-checking uses loop invariants in order to reduce\nthe p
roblem to an acyclic graph analysis instead of unrolling or\naccelerating
loops.\n\nI will present in this talk a new technique for generating polyn
omial\ninvariants\, divided in two independent parts : a procedure that re
duces\na class of loops containing polynomial assignments to linear loops
and a\nprocedure for generating inductive invariants for linear loops.\n\n
Both of these techniques have a polynomial complexity for a bounded\nnumbe
r of variables and we guarantee the completeness of the technique\nfor a b
ounded degree which we successfully implemented for C programs\nverificati
on as a Frama-C plug-in\, PILAT.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fixpoints in VASS: Results and Applications - Arnaud Sangnier\, I
RIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160926T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160926T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:109
DESCRIPTION:VASS (Vector Addition Systems with States)\, which are equival
ent to Petri nets\, are automata equipped with natural variables that can
be decremented or incremented. VASS are a powerful model which has been in
tensively studied in the last decades. Many verification techniques have b
een developed to analyse them and the frontier between the decidable and u
ndecidable problems related to VASS begins to be well known. One interesti
ng point is that the model-checking of linear temporal logics (like LTL o
r linear mu-calculus) is decidable for this model but this is not anymore
the case when considering branching time\ntemporal logics. However some re
strictions can be imposed on the logics and on the studied system in order
to regain decidability. In this talk\, we will present these results conc
erning the model-checking of\nVASS and the techniques leading to the decid
ability results. We will then show how these techniques and results can be
used to analyse some extensions of VASS with probabilities\, namely proba
bilistic VASS and VASS Markov Decision Processes.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Robustness against Consistency Models with Atomic Visibility - Gio
vanni Bernardi\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161003T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161003T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:110
DESCRIPTION:To achieve scalability\, modern Internet services often rely o
n distributed databases with consistency models for transactions weaker th
an serializability. At present\, application programmers often lack techni
ques to ensure that the weakness of these consistency models does not viol
ate application correctness.\nIn this talk I will present criteria to chec
k whether applications that rely on a database providing only weak consist
ency are robust\, i.e.\, behave as if they used a database providing seria
lizability\, and I will focus on a consistency model called Parallel Snaps
hot Isolation. The results I will outline handle systematically and unifor
mly several recently proposed weak consistency models\, as well as a mecha
nism for strengthening consistency in parts of an application.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Ideal Decompositions for Vector Addition Systems - Sylvain Schmitz
\, LSV - ENS Cachan
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161024T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161024T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:120
DESCRIPTION:Vector addition systems\, or equivalently Petri nets\, are one
of the\nmost popular formal models for the representation and the analysi
s\nof parallel processes. Many problems for vector addition systems are\nk
nown to be decidable thanks to the theory of well-structured\ntransition s
ystems. Indeed\, vector addition systems with\nconfigurations equipped wit
h the classical point-wise ordering are\nwell-structured transition system
s. Based on this observation\,\nproblems like coverability or termination
can be proven\ndecidable. However\, the theory of well-structured transiti
on systems\ndoes not explain the decidability of the reachability problem.
In\nthis presentation\, we show that runs of vector addition systems can\
nalso be equipped with a well quasi-order. This observation provides\na un
ified understanding of the data structures involved in solving\nmany probl
ems for vector addition systems\, including the central\nreachability prob
lem. \n\nJoint work with Jérôme Leroux.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Liveness of Randomised Parameterised Systems under Arbitrary Sched
ulers - Philipp Rümmer\, University of Uppsala
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161114T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161114T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:142
DESCRIPTION:e consider the problem of verifying liveness for systems with
a finite\,\nbut unbounded\, number of processes\, commonly known as\nparam
eterised systems. Typical examples of such systems include\ndistributed pr
otocols (e.g. for the dining philosopher problem).\nUnlike the case of ver
ifying safety\, proving liveness is still\nconsidered extremely challengin
g\, especially in the presence of\nrandomness in the system. In this paper
we consider liveness under\narbitrary (including unfair) schedulers\, whi
ch is often considered a\ndesirable property in the literature of self-sta
bilising systems. In\nthis paper we introduce an automatic method of provi
ng liveness\nfor randomised parameterised systems under arbitrary schedule
rs.\nViewing liveness as a two-player reachability game (between Scheduler
\nand Process)\, our method is a CEGAR approach that synthesises a progres
s\nrelation for Process that can be symbolically represented as a\nfinite-
state automaton. The method incrementally constructs a\nprogress relation\
, exploiting both Angluin's $L*$ algorithm and\nSAT-solvers. Our experimen
ts show that our algorithm is able to prove\nliveness automatically for we
ll-known randomised distributed protocols\,\nincluding Lehmann-Rabin Rando
mised Dining Philosopher Protocol and\nrandomised self-stabilising protoco
ls (such as the Israeli-Jalfon\nProtocol). To the best of our knowledge\,
this is the first\nfully-automatic method that can prove liveness for rand
omised protocols.\n\nJoint work with Anthony W. Lin.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Pragmatic Bug-finding Approach for Concurrent Programs - Gennaro
Parlato\, University of Southampton
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161124T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161124T160000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:154
DESCRIPTION:Concurrency poses a major challenge for program verification\,
but it can also offer an opportunity to scale when subproblems can be ana
lysed in parallel. We propose a parameterizable code-to-code translation t
o generate a set of simpler program variants such that each interleaving o
f the program is captured by at least one of them. These variants can then
be checked autonomously in parallel. Our approach is independent of the t
ool that is chosen for the final analysis\, it is compatible with weak mem
ory models\, and it amplifies the effectiveness of existing tools\, making
them find bugs faster and with fewer resources. We do our experiments usi
ng Lazy-CSeq as off-the-shelf final verifier and demonstrate that our appr
oach is able to find bugs in the hardest known concurrency benchmarks in a
matter of minutes where other dynamic and static tools fail to conclude.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:First-order logic with reachability for infinite-state systems - G
eorg Zetzsche\, LSV\, ENS Cachan
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161128T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161128T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:155
DESCRIPTION:First-order logic with the reachability predicate (FOR) is an
important means of specification in system analysis. Its decidability stat
us is known for some individual types of infinite-state systems such as pu
shdown (decidable) and vector addition systems (undecidable).\n\nThis work
aims at a general understanding of which types of systems admit decidabil
ity. As a unifying model\, we employ valence systems over graph monoids\,
which feature a finite-state control and are parameterized by a monoid to
represent their storage mechanism. As special cases\, this includes push
down systems\, various types of counter systems (such as vector addition s
ystems) and combinations thereof. Our main result is a characterization of
those graph monoids where FOR is decidable for the resulting\ntransition
systems.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:SyTeCi: Symbolic\, Temporal and Circular reasoning for automatic p
roofs of contextual equivalence - Guilhem Jaber\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161205T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161205T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:157
DESCRIPTION:Operational Techniques (Kripke Logical Relations and Environme
ntal/Open/Parametric Bisimulations) have matured enough to become now form
idable tools to prove contextual equivalence of effectful higher-order pro
grams. However\, it is not yet possible to automate such proofs -- the pro
blem being of course in general undecidable.\nIn this talk\, we will see h
ow to take the best of these techniques to design an automatic procedure w
hich is able many non-trivial examples of equivalence\, including most of
the examples from the literature.\nThe talk will describe the main ingredi
ents of this method:\n- Symbolic reduction to evaluate of programs\,\n- Tr
ansition systems of heap invariants\, as used with Kripke Logical Relation
s\,\n- Temporal logic to abstract over the control flow between the progra
m and its environment\,\n- Circular proofs to automate the reasoning over
recursive functions.\nUsing them\, we will see how we can reduce contextua
l equivalence to the problem of non-reachability in some automatically gen
erated transition systems of invariants.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Exposing Errors Related to Weak Memory in GPU Applications - Alast
air Donaldson\, Imperial College London
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161209T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161209T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:162
DESCRIPTION:In this presentation\, I will describe a project led by my PhD
student Tyler Sorensen\, on the systematic design of a testing environmen
t that uses stressing and fuzzing to reveal errors in GPU applications tha
t arise due to weak memory effects. This approach is evaluated across seve
ral CUDA applications that use fine-grained concurrency\, on seven GPUs sp
anning three Nvidia architectures. The results show that applications that
rarely\, or never\, exhibit errors related to weak memory when executed n
atively can readily exhibit these errors when executed in the testing envi
ronment. The testing environment also provides a means to identify the roo
t causes of erroneous weak effects\, and automatically suggests how to ins
ert fences that experimentally eliminate these errors. This empirical fenc
e insertion method carries significantly lower overhead\, in terms of exec
ution time and energy consumption\, than a more conservative\, guaranteed-
sound approach.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hierarchical Shape Abstraction for Analysis of Free-List Memory Al
locators (a logic-based approach) - Bin Fang\, IRIF(Paris)\, ECNU (China)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20161212T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20161212T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:167
DESCRIPTION:We propose a hierarchical abstract domain for the analysis of
free list memory allocators that tracks shape and numerical properties abo
ut both the heap and the free lists. Our domain is based on Separation Log
ic extended with predicates that capture the pointer arithmetics constrain
ts for the heap list and the shape of the free list. These predicates are
combined using a hierarchical composition operator to specify the overlapp
ing of the heap list by the free list. In addition to expressiveness\, thi
s operator leads to a compositional and compact representation of abstract
values and simplifies the implementation of the abstract domain. The shap
e constraints are combined with numerical constraints over integer arrays
to track properties about the allocation policies (best-fit\, first-fit\,
etc). Such properties are out of the scope of the existing analyzers. We i
mplemented this domain and we show its effectiveness on several implementa
tions of free list allocators.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Analysing Snapshot Isolation - Andrea Cerone\, Imperial College Lo
ndon
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170123T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170123T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:186
DESCRIPTION:Snapshot isolation (SI) is a widely used consistency model for
transaction processing\, implemented by most major databases and some of
transactional memory systems. Unfortunately\, its classical definition is
given in a low-level operational way\, by an idealised concurrency-control
algorithm\, and this complicates reasoning about the behaviour of applica
tions running under SI. We give an alternative specification to SI that ch
aracterises it in terms of transactional dependency graphs of Adya et al.\
, generalising serialization graphs. Unlike previous work\, our characteri
sation does not require adding additional information to dependency graphs
about start and commit points of transactions. We then exploit our specif
ication to obtain two kinds of static analyses. The first one checks when
a set of transactions running under SI can be chopped into smaller pieces
without introducing new behaviours\, to improve performance. The other ana
lysis checks whether a set of transactions running under a weakening of SI
behaves the same as when it running under SI.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lazy Reachability Analysis in Distributed Systems - Loig Jezequel\
, L2SN - Nantes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170220T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170220T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:202
DESCRIPTION:We address the problem of reachability in distributed systems\
, modelled as networks of finite automata and propose and prove a new algo
rithm to solve it efficiently in many cases. This algorithm allows to deco
mpose the reachability objective among the components\, and proceeds by co
nstructing partial products by lazily adding new components when required.
It thus constructs more and more precise over-approximations of the compl
ete product. This permits early termination in many cases\, in particular
when the objective is not reachable\, which often is an unfavorable case i
n reachability analysis. We have implemented this algorithm in a first pro
totype and provide some very encouraging experimental results.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Monitoring: Qualitative and Quantitative\, Real and Virtual\, Onli
ne and Offline - Oded Maler\, CNRS and University of Grenoble-Alpes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170227T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170227T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:205
DESCRIPTION:In this talk I will present some of the research I have been i
nvolved in concerning the specification and monitoring of timed\, continuo
us and hybrid behaviors using formalism such as Signal Temporal Logic and
Timed Regular Expressions. I will discuss the similarities and differences
between properties/assertions and other “measures” which are used in
many application domains to evaluate behaviors\, as well as the difference
between monitoring real systems during their execution and monitoring sim
ulated models during the system design phase.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Concurrent Data Structures Linked in Time - Germán Andrés Delbia
nco\, IMDEA Madrid
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170306T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170306T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:211
DESCRIPTION:Arguments about correctness of a concurrent data structure are
typically carried out by using the notion of linearizability and specifyi
ng the linearization points of the data structure's procedures. Such argum
ents are often cumbersome as the linearization points' position in time ca
n be dynamic (depend on the interference\, run-time values and events from
the past\, or even future)\, non-local (appear in procedures other than t
he one considered)\, and whose position in the execution trace may only be
determined after the considered procedure has already terminated.\n\nIn t
his talk I will present a new method\, based on a separation-style logic\,
for reasoning about concurrent objects with such linearization points. We
embrace the dynamic nature of linearization points\, and encode it as par
t of the data structure's auxiliary state\, so that it can be dynamically
modified in place by auxiliary code\, as needed when some appropriate run-
time event occurs.\n\nWe have named the idea linking-in-time\, because it
reduces temporal reasoning to spatial reasoning. For example\, modifying a
temporal position of a linearization point can be modeled similarly to a
pointer update in separation logic. Furthermore\, the auxiliary state prov
ides a convenient way to concisely express the properties essential for re
asoning about clients of such concurrent objects. In order to illustrate o
ur approach\, I will illustrate its application to verify (mechanically in
Coq) an intricate optimal snapshot algorithm\, due to Jayanti.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Promising Semantics for Relaxed-Memory Concurrency - Ori Lahav\,
MPI Kaiserslautern
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170313T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170313T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:212
DESCRIPTION:Despite many years of research\, it has proven very difficult
to develop a memory model for concurrent programming languages that adequa
tely balances the conflicting desiderata of programmers\, compilers\, and
hardware. In this paper\, we propose the first relaxed memory model that (
1) accounts for nearly all the features of the C++11 concurrency model\, (
2) provably validates a number of standard compiler optimizations\, as wel
l as a wide range of memory access reorderings that commodity hardware may
perform\, (3) avoids bad “out-of-thin-air” behaviors that break invar
iant-based reasoning\, (4) supports “DRF” guarantees\, ensuring that p
rogrammers who use sufficient synchronization need not understand the full
complexities of relaxed-memory semantics\, and (5) defines the semantics
of racy programs without relying on undefined behaviors\, which is a prere
quisite for applicability to type-safe languages like Java. \nThe key nove
l idea behind our model is the notion of promises: a thread may promise to
execute a write in the future\, thus enabling other threads to read from
that write out of order. Crucially\, to prevent out-of-thin-air behaviors\
, a promise step requires a thread-local certification that it will be pos
sible to execute the promised write even in the absence of the promise. To
establish confidence in our model\, we have formalized most of our key re
sults in Coq.\n\nJoint work with Jeehoon Kang\, Chung-Kil Hur\, Viktor Vaf
eiadis\, and Derek Dreyer\, recently presented at POPL'17
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Proving Liveness of Parameterized Programs - Andreas Podelski\, Un
iversity of Freiburg
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170320T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170320T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:227
DESCRIPTION:Correctness of multi-threaded programs typically requires that
they satisfy liveness properties. For example\, a program may require tha
t no thread is starved of a shared resource\, or that all threads eventual
ly agree on a single value. This paper presents a method for proving that
such liveness properties hold. Two particular challenges addressed in this
work are that (1) the correctness argument may rely on global behaviour o
f the system (e.g.\, the correctness argument may require that all threads
collectively progress towards “the good thing” rather than one thread
progressing while the others do not interfere)\, and (2) such programs ar
e often designed to be executed by any number of threads\, and the desired
liveness properties must hold regardless of the number of threads that ar
e active in the program. This is joint work with Azadeh Farzan and Zachary
Kincaid and published at LICS 2016 (http://www.cs.princeton.edu/~zkincaid
/pub/lics16.pdf)
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lossy Channel Systems with Data. - Mohamed Faouzi Atig\, Uppsala U
niversity
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170327T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170327T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:230
DESCRIPTION:Lossy channel systems are a classical model with applications
ranging from the modelling of communication protocols to programs running
on weak memory models. All existing work assume that messages traveling in
side the channels are picked from a finite alphabet. In this talk\, we pre
sent two extensions of lossy channel systems. In the first part of the tal
k\, we extend lossy channel systems by assuming that each message is equip
ped with a clock representing the age of the message\, thus obtaining the
model of Timed Lossy Channel Systems (TLCS). We show that the state reacha
bility problem is decidable for TLCS.\n\nIn the second part of the talk\,
we extend lossy channel systems by considering systems that operate on a f
inite set of variables ranging over an infinite data domain. Furthermore\,
each message inside a channel is equipped with a data item representing i
ts value. Although we restrict the model by allowing the variables to be o
nly tested for (dis-)equality\, we show that the state reachability proble
m is undecidable. In light of this negative result\, we consider bounded-p
hase reachability\, where the processes are restricted to performing eithe
r send or receive operations during each phase. We show decidability of st
ate reachability in this case by computing a symbolic encoding of the set
of system configurations that are reachable from a given configuration.\n\
n\nThis talk is based on previous joint work with Parosh Aziz Abdula\, Jo
nathan Cederberg and C. Aiswarya.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:The Erdös & Tarski theorem. A new class of WSTS without WQO. - Al
ain Finkel\, LSV\, ENS Cachan
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170522T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170522T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:258
DESCRIPTION:We present the ideal framework which was recently used to obta
in new deep results on Petri nets and extensions. We will present the proo
f of the famous but unknown Erdös-Tarski theorem. We argue that the theor
y of ideals prompts a renewal of the theory of WSTS by providing a way to
define a new class of monotonic systems\, the so-called Well Behaved Trans
ition Systems\, which properly contains WSTS\, and for which coverability
is still decidable by a forward algorithm.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Inductive Termination Proofs by Transition Predicate Abstraction a
nd their relationship to the Size-Change Abstraction - Florian Zuleger\, T
U Wien
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170523T153000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170523T163000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:262
DESCRIPTION:The last decade has seen renewed interest in automated techniq
ues for proving the termination of programs. A popular termination criteri
on is based on the covering of the transitive hull of the transition relat
ion of a program by a finite number of well-founded relations. In an autom
ated\nanalysis\, this termination criterion is usually established by an i
nductive proof using transition predicate abstraction. Such termination pr
oofs have the structure of a finite automaton. These automata\, which we c
all transition automata\, are the central object of study in this talk.\nO
ur main results are as follows: (1) A previous criterion for termination a
nalysis with transition automata is not complete\; we provide a complete c
riterion. (2) We show how to bound the height of the transition relation o
f the program using the termination proof by transition predicate abstract
ion. This result has applications in the automated complexity analysis of
programs. (3) We show that every termination proof by transition predicate
abstraction gives rise to a termination proof by the size-change abstract
ion\; this connection is crucial to obtain results (1) and (2) from previo
us results on the size-change abstraction. Further\, our result establishe
s that transition predicate abstraction and size-change abstraction have t
he same expressivity for automated termination proofs.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Sound and Complete Mutation-Based Program Repair - Orna Grumberg\,
Technion\, Israel
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170601T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170601T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:263
DESCRIPTION:This work presents a novel approach for automatically repairin
g an erroneous program with respect to a given set of assertions. Programs
are repaired using a predefined set of mutations. We refer to a bounded n
otion of correctness\, even though\, for a large enough bound all returned
programs are fully correct. To ensure no changes are made to the original
program unless necessary\, if a program can be repaired by applying a set
of mutations $Mut$\, then no superset of $Mut$ is later considered. Progr
ams are checked in increasing number of mutations\, and every minimal repa
ired program is returned as soon as found.\n \nWe impose no assumptions on
the number of erroneous locations in the program\, yet we are able to gua
rantee soundness and completeness. That is\, we assure that a program is r
eturned iff it is minimal and bounded correct.\n \nSearching the space of
mutated programs is reduced to searching unsatisfiable sets of constraints
\, which is performed efficiently using a sophisticated cooperation betwee
n SAT and SMT solvers. Similarities between mutated programs are exploited
in a new way\, by using both the SAT and the SMT solvers incrementally.\n
\nWe implemented a prototype of our algorithm\, compared it with a state-
of-the-art repair tool and got very encouraging results.\nThis is a joint
work with Bat-Chen Rothenberg.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Tasks\, objects\, and the notion of a distributed problem - Sergio
Rajsbaum\, UNAM Mexico
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170606T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170606T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:264
DESCRIPTION:The universal computing model of Turing\, which was central to
the birth of modern computer science\, identified also the essential noti
on of a problem\, as an input output function to be computed by a Turing m
achine. In distributed computing\, \\emph{tasks} are the equivalent of a f
unction: each process gets only part of the input\, and computes part of t
he output after communicating with other processes.\n\nIn distributed comp
uting tasks have been studied from early on\, in parallel\, but independen
tly of \\emph{sequential objects}. While tasks explicitly state what might
happen when a set of processes run concurrently\, sequential objects onl
y specify what happens when processes run sequentially. Indeed\, many dist
ributed problems considered in the literature\, seem to have no natural sp
ecification neither as tasks nor as sequential objects. I will concentrate
on our recent work on interval-linearizability\, a notion we introduced t
o specify objects more general than the usual sequential objects. I will
describe the bridges we establish between these two classical paradigms\,
and our discussions about what is a distributed problem\, and what it mean
s to solve it.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Simple Framework for Verifying Concurrent Search Structures - Th
omas Wies\, New York University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170612T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170612T150000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:273
DESCRIPTION:We present an abstract framework for verifying concurrent algo
rithms on search data structures that support dictionaries. The framework
can be specialized to every search data structure we know\, from linked li
sts to complex B-trees. We obtain this framework by instantiating RGSep\,
which is a program logic that combines rely-guarantee reasoning and separa
tion logic. RGSep is parameterized by a so-called resource algebra\, which
is typically the standard heap model of separation logic. Instead of usin
g the standard heap model\, we develop a new resource algebra that enables
compositional reasoning about search graphs. Using this search graph mode
l\, we obtain simple correctness proofs of complex concurrent dictionary a
lgorithms. The algorithms and proofs abstract from the specific search dat
a structure that the algorithm operates on and can then be refined to a co
ncrete data structure implementation.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:New Applications of Software Synthesis: Verification of Configurat
ion Files and Firewalls Repair - Ruzica Piskac\, Yale University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170622T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170622T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:279
DESCRIPTION:In this talk we present a new approach for verification for co
nfiguration files. Software failures resulting from configuration errors h
ave become commonplace as modern software systems grow increasingly large
and more complex. The lack of language constructs in configuration files\,
such as types and grammars\, has directed the focus of a configuration fi
le verification towards building post-failure error diagnosis tools. We de
scribe a framework which analyzes data sets of correct configuration files
and synthesizes rules for building a language model from the given data s
et. The resulting language model can be used to verify new configuration f
iles and detect errors in them.\n\nWe also outline a systematic effort tha
t can automatically repair firewalls\, using the programming by example ap
proach. Firewalls are widely employed to manage and control enterprise net
works. Because enterprise-scale firewalls contain hundreds or thousands of
policies\, ensuring the correctness of firewalls - whether the policies i
n the firewalls meet the specifications of their administrators - is an im
portant but challenging problem. In our approach\, after an administrator
observes undesired behavior in a firewall\, she may provide input/output e
xamples that comply with the intended behavior. Based on the given example
s\, we automatically synthesize new firewall rules for the existing firewa
ll. This new firewall correctly handles packets specified by the examples\
, while maintaining the rest of the behavior of the original firewall.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Paxos Made EPR --- Decidable Reasoning about Distributed Consensus
- Giuliano Losa\, UCLA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20170628T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20170628T150000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:281
DESCRIPTION:Distributed protocols such as Paxos play an important role in
many computer systems. Therefore\, a bug in a distributed protocol may hav
e tremendous effects. Accordingly\, a lot of effort has been invested in v
erifying such protocols. However\, checking invariants of such protocols i
s undecidable and hard in practice\, as it requires reasoning about an unb
ounded number of nodes and messages. Moreover\, protocol actions and invar
iants involve higher-order concepts such as set cardinalities\, arithmetic
\, and complex quantification.\n\nThis paper makes a step towards automati
c verification of such protocols. We aim at a technique that can verify co
rrect protocols and identify bugs in incorrect protocols. To this end\, we
develop a methodology for deductive verification based on effectively pro
positional logic (EPR)---a decidable fragment of first-order logic (also k
nown as the Bernays-Sch\\"onfinkel-Ramsey class). In addition to decidabil
ity\, EPR also enjoys the finite model property\, allowing to display viol
ations as finite structures which are intuitive for users. Our methodology
involves modeling protocols using general (uninterpreted) first-order log
ic\, and then systematically transforming the model to obtain a model and
an inductive invariant that are decidable to check. The steps of the trans
formations are also mechanically checked\, ensuring the soundness of the m
ethod. We have used our methodology to verify the safety of Paxos\, and se
veral of its variants\, including Multi-Paxos\, Vertical Paxos\, Fast Paxo
s and Flexible Paxos. To the best of our knowledge\, this work is the firs
t to verify these protocols using a decidable logic\, and the first formal
verification of Vertical Paxos and Fast Paxos. \n\nThis is joint work wit
h O. Padon\, M. Sagiv\, and S. Shoham.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Verifying Robustness of Event-Driven Asynchronous Programs Against
Concurrency - Ahmed Bouajjani\, IRIF - Université Paris Diderot
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171002T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171002T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:305
DESCRIPTION:We define a correctness criterion\, called robustness against\
nconcurrency\, for a class of event-driven asynchronous programs that\nare
at the basis of modern UI frameworks in Android\, iOS\, and\nJavascript.
A program is robust when all possible behaviors admitted\nby the program u
nder arbitrary procedure and event interleavings are\nadmitted even if asy
nchronous procedures (respectively\, events) are\nassumed to execute seria
lly\, one after the other\, accessing shared\nmemory in isolation. We char
acterize robustness as a conjunction of\ntwo correctness criteria: event-s
erializability (i.e.\, events can be\nseen as atomic) and event-determinis
m (executions within each event\nare insensitive to the interleavings betw
een concurrent tasks\ndynamically spawned by the event). Then\, we provide
efficient\nalgorithms for checking these two criteria based on polynomial
\nreductions to reachability problems in sequential programs. This\nresult
is surprising because it allows to avoid explicit handling of\nall concur
rent executions in the analysis\, which leads to an important\ngain in com
plexity. We demonstrate via case studies on Android apps\nthat the typical
mistakes programmers make are captured as robustness\nviolations\, and th
at violations can be detected efficiently using our\napproach. \n\nJoint w
ork with Michael Emmi\, Constantin Enea\, Burcu Kulahcioglu\nOzkan\, and S
erdar Tasiran.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Polynomial Analysis Algorithms for Free-Choice Workflow Nets - Jav
ier Esparza\, Technische Universität München
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171009T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171009T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:306
DESCRIPTION:Workflow Petri nets are a successful formalism for modelling\,
\nsimulating\, and analyzing business processes. In this area\,\nfree-choi
ce workflow nets play an important role: Core formalisms\nfor business pro
cesses can be translated into free-choice nets\,\nand many industrial mode
ls are free-choice.\n\nWhile the state space of a free-choice net can grow
exponentially\nin its number of nodes\, numerous control-flow properties
can still\nbe decided in polynomial time. However\, these decision algorit
hms\ncannot be extended to workflow nets with data. We present a new\nanal
ysis technique\, based on reduction rules\, that can be applied\nto workfl
ow nets with data\, costs\, or probabilities. In particular\,\nwe give a p
olynomial algorithm to compute the expected cost of sound\nfree-choice wor
kflow nets.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Proving linearizability using forward simulations - Suha Mutluergi
l\, Koç University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171030T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171030T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:307
DESCRIPTION:Linearizability is the standard correctness criterion for conc
urrent\ndata structures such as stacks and queues. It allows to establish\
nobservational refinement between a concurrent implementation and an\natom
ic reference implementation.\n\nProving linearizability requires identifyi
ng linearization points for\neach method invocation along all possible com
putations\, leading to\nvalid sequential executions\, or alternatively\, e
stablishing forward\nand backward simulations. In both cases\, carrying ou
t proofs is hard\nand complex in general. In particular\, backward reasoni
ng is difficult\nin the context of programs with data structures\, and str
ategies for\nidentifying statically linearization points cannot be defined
for all\nexisting implementations. In this paper\, we show that\, contra
ry to\ncommon belief\, many such complex implementations\, including\, e.g
.\, the\nHerlihy & Wing Queue and the Time-Stamped Stack\, can be proved c
orrect\nusing only forward simulation arguments. This leads to simple and\
nnatural correctness proofs for these implementations that are amenable\nt
o automation.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Verifying Equivalence of Spark Programs - Noam Rineztky\, Tel-Aviv
University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171016T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171016T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:320
DESCRIPTION:Apache Spark is a popular framework for writing large scale da
ta\nprocessing applications. Our long term goal is to develop automatic\nt
ools for reasoning about Spark programs. This is challenging because\nSpar
k programs combine database-like relational algebraic operations\nand aggr
egate operations\, corresponding to (nested) loops\, with User\nDefined Fu
nctions (UDFs).\n\nIn this paper\, we present a novel SMT-based technique
for verifying\nthe equivalence of Spark programs. We model Spark as a prog
ramming\nlanguage whose semantics imitates Relational Algebra queries (wit
h\naggregations) over bags (multisets) and allows for UDFs expressible in\
nPresburger Arithmetics. We prove that the problem of checking\nequivalenc
e is undecidable even for programs which use a single\naggregation operato
r. Thus\, we present sound techniques for verifying\nthe equivalence of in
teresting classes of Spark programs\, and show\nthat it is complete under
certain restrictions. We implemented our\ntechnique\, and applied it to a
few small\, but intricate\, test cases.\n\nJoint work with: Shelly Grossma
n\, Sara Cohen\, Shachar Itzhaky\, and\nMooly Sagiv Presented in CAV’17
\n\nPaper: http://www.cs.tau.ac.il/~maon/pubs/2017-cav.pdf
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:FocaLiZe and Dedukti to the Rescue for Proof Interoperability - Ra
phaël Cauderlier\, IRIF - Université Paris Diderot
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171023T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171023T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:321
DESCRIPTION:Numerous contributions have been made for some years to allow
users to\nexchange formal proofs between different provers. The main\nprop
ositions consist in ad hoc pointwise translations\, e.g. between\nHOL Ligh
t and Isabelle in the Flyspeck project or uses of more or less\ncomplete c
ertificates. We propose a methodology to combine proofs\ncoming from diffe
rent theorem provers. This methodology relies on the\nDedukti logical fram
ework as a common formalism in which proofs can be\ntranslated and combine
d. To relate the independently developed\nmathematical libraries used in p
roof assistants\, we rely on the\nstructuring features offered by FoCaLiZe
\, in particular parameterized\nmodules and inheritance to build a formal
library of transfer theorems\ncalled MathTransfer. We finally illustrate t
his methodology on the\nSieve of Eratosthenes\, which we prove correct usi
ng HOL and Coq in\ncombination.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Effective Stateless Model Checking for C/C++ Concurrency - Viktor
Vafeiadis\, Max Planck Institute for Software Systems (MPI-SWS)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171113T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171113T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:335
DESCRIPTION:I will present a stateless model checking algorithm for verify
ing concurrent programs running under RC11\, a repaired version of the C/C
++11 memory model without dependency cycles. Unlike previous approaches\,
which enumerate thread interleavings up to some partial order reduction im
provements\, our approach works directly on execution graphs and (in the a
bsence of RMW instructions and SC atomics) avoids redundant exploration by
construction. We have implemented a model checker\, called RCMC\, based
on this approach and applied it to a number of challenging concurrent prog
rams. Our experiments confirm that RCMC is significantly faster\, scales b
etter than other model checking tools\, and is also more resilient to smal
l changes in the benchmarks.\n\n(This is joint work with Michalis Kokologi
annakis\, Ori Lahav\, and Konstantinos Sagonas\, and will appear at POPL'1
8.)
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Euler’s Method Applied to the Control of Switched Systems - Laur
ent Fribourg\, LSV\, CNRS & ENS de Cachan
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171120T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171120T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:339
DESCRIPTION:Hybrid systems are a powerful formalism for modeling and reaso
ning about cyber-physical systems. They mix the continuous and discrete na
tures of the evolution of computerized systems. Switched systems are a spe
cial kind of hybrid systems\, with restricted discrete behaviours: those s
ystems only have finitely many different modes of (continuous) evolution\,
with isolated switches between modes. Such systems provide a good balance
between expressiveness and controllability\, and are thus in widespread u
se in large branches of industry such as power electronics and automotive
control. The control law for a switched system defines the way of selectin
g the modes during the run of the system. Controllability is the problem o
f (automatically) synthezing a control law in order to satisfy a desired p
roperty\, such as safety (maintaining the variables within a given zone) o
r stabilisation (confinement of the variables in a close neighborhood arou
nd an objective point). In order to compute the control of a switched syst
em\, we need to compute the solutions of the differential equations govern
ing the modes. Euler’s method is the most basic technique for approximat
ing such solutions. We present here an estimation of the Euler’s method
local error\, using the notion of “one-sided Lispchitz constant’’ fo
r modes. This yields a general synthesis approach which can encompass unce
rtain parameters\, local information and stochastic noise.\n\nWe will sket
ch out how the approach relates with other symbolic methods based on inter
val arithmetic and Lyapunov functions. We will also present some applicati
ve examples which illustrate its advantages and limitations.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Checking Linearizability of Concurrent Priority Queues - Chao Wang
\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180115T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180115T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:340
DESCRIPTION:Efficient implementations of concurrent objects such as atomic
\ncollections are essential to modern computing. Unfortunately their\ncorr
ectness criteria — linearizability with respect to given ADT\nspecificat
ions — are hard to verify. Verifying linearizability is\nundecidable in
general\, even on classes of implementations where the\nusual control-stat
e reachability is decidable. In this work we\nconsider concurrent priority
queues which are fundamental to many\nmulti-threaded applications like ta
sk scheduling or discrete event\nsimulation\, and show that verifying line
arizability of such\nimplementations is reducible to control-state reachab
ility. This\nreduction entails the first decidability results for verifyin
g\nconcurrent priority queues with an unbounded number of threads\, and it
\nenables the application of existing safety-verification tools for\nestab
lishing their correctness.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Congruence Preservation\, Lattices and Recognizability - Irène Gu
essarian\, IRIF - Unviersité Paris Diderot
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171211T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171211T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:347
DESCRIPTION:Looking at some monoids and (semi)rings (natural numbers\, int
egers and\np-adic integers)\, and more generally\, residually finite algeb
ras (in a\nstrong sense)\, we prove the equivalence of two ways for a func
tion on\nsuch an algebra to behave like the operations of the algebra. The
\nfirst way is to preserve congruences or stable preorders. The second\nwa
y is to demand that preimages of recognizable sets belong to the\nlattice
or the Boolean algebra generated by the preimages of\nrecognizable sets by
“derived unary operations” of the algebra (such\nas translations\, qu
otients\,...).
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:The Spirit of Ghost Code - Léon Gondelman\, Radboud University\,
The Netherlands
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171128T133000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171128T143000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:365
DESCRIPTION:In the context of deductive program verification\, ghost code
is part\nof the program that is added for the purpose of specification. Gh
ost\ncode must not interfere with regular code\, in the sense that it can
be\nerased without any observable difference in the program outcome. In\np
articular\, ghost data cannot participate in regular computations and\ngho
st code cannot mutate regular data or diverge.\n\nThe idea exists in the f
olklore since the early notion of auxiliary\nvariables and is implemented
in many state-of-the-art program\nverification tools. However\, a rigorous
definition and treatment of\nghost code is surprisingly subtle and few fo
rmalizations exist.\n\nIn this talk\, we describe a simple ML-style progra
mming language with\nmutable state and ghost code. Non-interference is en
sured by a type\nsystem with effects\, which allows\, notably\, the same d
ata types and\nfunctions to be used in both regular and ghost code. We de
fine the\nprocedure of ghost code erasure and we prove its safety using\nb
isimulation. A similar type system\, with numerous extensions which we\nbr
iefly discuss\, is implemented in the program verification\nenvironment Wh
y3.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Constrained Horn clauses for automatic program verification: the h
igher-order case - Luke Ong\, University of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20171207T160000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20171207T170000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:366
DESCRIPTION:Following Björner\, McMillan and Rybalchenko\, we develop an
approach to\nthe automatic verification of higher-order functional program
s based\non constrained Horn clauses. We introduce constrained Horn clause
s in\nhigher-order logic\, and decision problems concerning their\nsatisfi
ability and the safety verification of higher-order programs.\nWe show tha
t\, although satisfiable systems of higher-order clauses do\nnot generally
have least models\, there is a notion of canonical model\nobtained via a
reduction to a problem concerning a kind of monotone\nlogic program. Follo
wing work in higher-order program verification\, we\ndevelop a refinement
type system in order to reason about and automate\nthe search for models.
This provides a sound but incomplete method for\nsolving the decision prob
lem. Finally\, we show that an extension of\nthe decision problem in which
refinement types are used directly as\nguards on existential quantifiers
can be reduced to the original\nproblem. This result can be used to show t
hat properties of\nhigher-order functions that are definable using refinem
ent types are\nalso expressible using higher-order constrained Horn clause
s. (Joint\nwork with Toby Cathcart Burn and Steven Ramsay.)
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Proofs of graph algorithms with automation and their readability -
Jean-Jacques Lévy\, IRIF & INRIA
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180108T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180108T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:367
DESCRIPTION:In this talk\, we present a proof of correctness for an algori
thm computing strongly connected components in a directed graph by Tarjan
[1972]. It will be the starting point of a discussion about the readabilit
y of formal proofs. This proof was achieved with the Why3 system and the C
oq/ssreflect proof assistant. The same proof was redone fully in Coq/ssre
flect and Isabelle/HOL.\n\nThis is joint work with Ran Chen and was presen
ted at VSTTE 2017. The Coq and Isabelle proofs were achieved by Cyril Cohe
n\, Laurent Théry and Stephan Merz.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fault-Tolerant Decentralized Runtime Monitoring - Pierre Fraigniau
d\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160229T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160229T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:397
DESCRIPTION:Runtime verification is aiming at extracting information from
a running system\, and using it to detect and possibly react to behaviors
violating a given correctness property. Decentralized runtime verification
involves a set of monitors observing the behavior of the underlying syste
m. In this talk\, the investigation of decentralized runtime verification
in which not only the elements of the observed system\, but also the monit
ors themselves are subject to failures will be presented. In this context\
, it is unavoidable that the unreliable monitors may have different views
of the underlying system\, and therefore may have different valuations of
the correctness property. We characterize the number of valuations require
d for monitoring a given correctness property in a decentralized manner. O
ur lower bound is independent of the logic used for specifying the correct
ness property\, as well as of the way the set of valuations returned by th
e monitors is globally interpreted. Moreover\, our lower bound is tight in
the sense that we design a distributed protocol enabling any given set of
monitors to verify any given correctness property using as many different
valuations as the one given by this lower bound. Joint work with: Sergio
Rajsbaum (UNAM\, Mexico) and Corentin Travers (LaBRI\, Bordeaux).
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Frama-C\, a collaborative and extensible framework for C code anal
ysis - Julien Signoles\, CEA-LIST
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160307T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160307T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:398
DESCRIPTION:Frama-C is a source code analysis platform that aims at conduc
ting verification of industrial-size C programs. It provides its users wit
h a collection of plug-ins that perform static analysis\, deductive verifi
cation\, testing and monitoring\, for safety- and security-critical softwa
re. Collaborative verification across cooperating plug-ins is enabled by t
heir integration on top of a shared kernel and datastructures\, and their
compliance to a common specification language. This talk presents a consol
idated view of the platform\, its main and composite analyses\, and some o
f its industrial achievements. It focuses on its specification language AC
SL\, and on different ways to verify ACSL specifications through static an
d dynamic analyses.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Formal methods for the verification of distributed algorithms - Pa
ul Gastin\, LSV
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20160314T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20160314T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:399
DESCRIPTION:We introduce an automata-theoretic method for the verification
of distributed algorithms running on ring networks. In a distributed algo
rithm\, an arbitrary number of processes cooperate to achieve a common goa
l (e.g.\, elect a leader). Processes have unique identifiers (pids) from a
n infinite\, totally ordered domain. An algorithm proceeds in synchronous
rounds\, each round allowing a process to perform a bounded sequence of ac
tions such as send or receive a pid\, store it in some register\, and comp
are register contents wrt. the associated total order. An algorithm is sup
posed to be correct independently of the number of processes. To specify c
orrectness properties\, we introduce a logic that can reason about process
es and pids. Referring to leader election\, it may say that\, at the end o
f an execution\, each process stores the maximum pid in some dedicated reg
ister. Since the verification of distributed algorithms is undecidable\, w
e propose an underapproximation technique\, which bounds the number of rou
nds. This is an appealing approach\, as the number of rounds needed by a d
istributed algorithm to conclude is often exponentially smaller than the n
umber of processes. We provide an automata-theoretic solution\, reducing m
odel checking to emptiness for alternating two-way automata on words. Over
all\, we show that round-bounded verification of distributed algorithms ov
er rings is PSPACE-complete. Based on a joint work with C. Aiswarya and Be
nedikt Bollig\, extended abstract at CONCUR’15: [[http://www.lsv.ens-cac
han.fr/~gastin/mes-publis.php?onlykey=ABG-concur15]].
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Synthesis of Distributed Algorithms with Parameterized Thresholds
Guards - Josef Widder\, TU Wien
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180122T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180122T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:420
DESCRIPTION:Fault-tolerant distributed algorithms are notoriously hard to
get right. I present an automated method that helps in that process: the d
esigner provides specifications (the problem to be solved) and a sketch of
a distributed algorithm that keeps arithmetic details unspecified. Our to
ol then automatically fills the missing parts. In particular\, I will cons
ider threshold-based distributed algorithms\, where a process has to wait
until the number of messages it receives reaches a certain threshold\, in
order to perform an action. Such algorithms are typically used for achievi
ng fault tolerance in distributed algorithms for broadcast\, atomic commit
ment\, or consensus. Using this method\, one can synthesize distributed al
gorithms that are correct for every number n of processes and every number
t of faults\, provided some resilience condition holds\, e.g.\, n > 3t. T
his approach combines recent progress in parameterized model checking of d
istributed algorithms---which I also address---with counterexample-guided
synthesis. \n\nThis is joint work with Marijana Lazić\, Igor Konnov\, and
Roderick Bloem.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Probabilistic Disclosure: Maximisation vs. Minimisation - Engel Le
faucheaux\, ENS Cachan / IRISA Rennes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180129T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180129T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:421
DESCRIPTION:We consider opacity questions where an observation function pr
ovides to an external attacker a view of the states along executions and s
ecret executions are those visiting some state from a fixed subset. Disclo
sure occurs when the observer can deduce from a finite observation that th
e execution is secret. In a probabilistic and nondeterministic setting\, w
here an internal agent can choose between actions\, there are two points o
f view\, depending on the status of this agent: the successive choices can
either help the attacker trying to disclose the secret\, if the system ha
s been corrupted\, or they can prevent disclosure as much as possible if t
hese choices are part of the system design. In the former situation\, corr
esponding to a worst case\, the disclosure value is the supremum over the
strategies of the probability to disclose the secret (maximisation)\, wher
eas in the latter case\, the disclosure is the infimum (minimisation). We
address quantitative problems (comparing the optimal value with a threshol
d) and qualitative ones (when the threshold is zero or one) related to bot
h forms of disclosure for a fixed or finite horizon. For all problems\, we
characterise their decidability status and their complexity. We discover
a surprising asymmetry: on the one hand optimal strategies may be chosen a
mong deterministic ones in maximisation problems\, while it is not the cas
e for minimisation. On the other hand\, for the questions addressed here\,
more minimisation problems than maximisation ones are decidable.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Programming and Proving with Distributed Protocols - Ilya Sergey\,
University College London\, UK
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180409T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180409T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:449
DESCRIPTION:Distributed systems play a crucial role in modern infrastructu
re\, but are notoriously difficult to implement correctly. This difficulty
arises from two main challenges: (a) correctly implementing core system c
omponents (e.g.\, two-phase commit)\, so all their internal invariants hol
d\, and (b) correctly composing standalone system components into function
ing trustworthy applications (e.g.\, persistent storage built on top of a
two-phase commit instance). Recent work has developed several approaches f
or addressing (a) by means of mechanically verifying implementations of co
re distributed components\, but no methodology exists to address (b) by co
mposing such verified components into larger verified applications. \n\nAs
a result\, expensive verification efforts for key system components are n
ot easily reusable\, which hinders further verification efforts. \n\n In m
y talk\, I will present Disel\, the first framework for implementation and
reusable compositional verification of distributed systems and their clie
nts\, all within the mechanized\, foundational context of the Coq proof as
sistant. \n\n In Disel\, users implement distributed systems using a domai
n specific language shallowly embedded in Coq and providing both high-leve
l programming constructs as well as low-level communication primitives. Co
mponents of composite systems are specified in Disel as protocols\, which
capture system-specific logic and disentangle system definitions from impl
ementation details. By virtue of Disel’s dependent type system\, well-ty
ped implementations always satisfy their protocols’ invariants and never
go wrong\, allowing users to verify system implementations interactively
using Disel’s Hoare-style Separation Logic\, which extends state-of-the-
art techniques for concurrency verification to the distributed setting.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Effective Random Testing for Concurrent and Distributed Programs -
Rupak Majumdar\, Max Planck Institute for Software Systems (MPI-SWS)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180319T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180319T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:450
DESCRIPTION:Random testing has proven to be an effective way to catch bugs
in distributed systems. This is surprising\, as the space of executions i
s enormous. We provide a theoretical justification of the effectiveness of
random testing under various "small depth" hypotheses. First\, we show a
general construction\, using the probabilistic method from combinatorics\,
that shows that whenever a random test covers a fixed coverage goal with
sufficiently high probability\, a small randomly-chosen set of tests achie
ves full coverage with high probability. In particular\, we show that our
construction can give test sets exponentially smaller than systematic enum
eration. Second\, based on an empirical study of many bugs found by rando
m testing in production distributed systems\, we introduce notions of test
coverage which capture the "small depth" hypothesis and are empirically e
ffective in finding bugs. Finally\, we show using combinatorial arguments
that for these notions of test coverage we introduce\, we can find a lowe
r bound on the probability that a random test covers a given goal. Our gen
eral construction then explains why random testing tools achieve good cove
rage---and hence\, find bugs---quickly.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Linearizability of Concurrent Data Structures via Order Extension
Theorems - Ana Sokolova\, Universität Salzburg\, Austria
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180528T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180528T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:451
DESCRIPTION:The semantics of concurrent data structures is usually given b
y a sequential specification and a consistency condition. Linearizability
is the most popular consistency condition due to its simplicity and genera
l applicability. Verifying linearizability is a difficult\, in general und
ecidable\, problem.\n\nIn this talk\, I will discuss the semantics of conc
urrent data structures and present recent order extension results (joint w
ork with Harald Woracek) that lead to characterizations of linearizability
in terms of violations\, a.k.a. aspects. The approach works for pools\, q
ueues\, and priority queues\; finding other applications is ongoing work.
In the case of pools and queues we obtain already known characterizations\
, but the proof method is new\, elegant\, and simple\, and we expect that
it will lead to deeper understanding of linearizability.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Provably secure compilation of side-channel countermeasures: the c
ase of cryptographic “constant-time” - Vincent Laporte\, IMDEA Softwar
e
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180208T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180208T113000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:452
DESCRIPTION:Software-based countermeasures provide effective mitigation ag
ainst\nside-channel attacks\, often with minimal efficiency and deployment
\noverheads. Their effectiveness is often amenable to rigorous analysis:\n
specifically\, several popular countermeasures can be formalized as\ninfor
mation flow policies\, and correct implementation of the\ncountermeasures
can be verified with state-of-the-art analysis and\nverification technique
s. However\, in absence of further justification\,\nthe guarantees only ho
ld for the language (source\, target\, or\nintermediate representation) on
which the analysis is performed.\n\nWe consider the problem of preserving
side-channel countermeasures by\ncompilation for cryptographic “constan
t-time”\, a popular countermeasure\nagainst cache-based timing attacks.
We present a general method\, based\non the notion of 2-simulation\, for p
roving that a compilation pass\npreserves the constant-time countermeasure
. Using the Coq proof\nassistant\, we verify the correctness of our method
and of several\nrepresentative instantiations.
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:20210731T070300Z
UID:504
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:When Good Components Go Bad: Formally Secure Compilation Despite D
ynamic Compromise - Cătălin Hriţcu\, INRIA Paris
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180226T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180226T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:521
DESCRIPTION:We propose a new formal criterion for secure compilation\, giv
ing strong end-to-end security guarantees for software components written
in unsafe\, low-level languages with C-style undefined behavior. Our crite
rion is the first to model _dynamic_ compromise in a system of mutually di
strustful components running with least privilege. Each component is prote
cted from all the others---in particular\, from components that have encou
ntered undefined behavior and become compromised. Each component receives
secure compilation guarantees up to the point when it becomes compromised\
, after which an attacker can take complete control over the component and
use any of its privileges to attack the remaining uncompromised component
s. More precisely\, we ensure that dynamically compromised components cann
ot break the safety properties of the system at the target level any more
than equally privileged components without undefined behavior already coul
d in the\nsource language.\n\nTo illustrate this model\, we build a secure
compilation chain for an unsafe language with buffers\, procedures\, and
components. We compile it to a simple RISC abstract machine with built-in
compartmentalization and provide thorough proofs\, many of them machine-ch
ecked in Coq\, showing that the compiler satisfies our secure compilation
criterion. Finally\, we show that the protection guarantees offered by the
compartmentalized abstract machine can be achieved at the machine-code le
vel using either software fault isolation or a tag-based reference monitor
.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Automata and Program Analysis - Thomas Colcombet\, IRIF & CNRS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180312T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180312T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:534
DESCRIPTION:This will be a presentation of a collaboration with Laure Davi
aud and Florian Zuleger. We show how recent results concerning quantitativ
e forms of automata help providing refined understanding of the properties
of a system (for instance\, a program). In particular\, combining the siz
e-change abstraction together with results concerning the asymptotic behav
ior of tropical automata yields extremely fine complexity analysis of some
pieces of code.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Automated Verification of Privacy-type Properties for Security Pro
tocols - Ivan Gazeau\, LORIA & INRIA Nancy - Grand Est
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180326T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180326T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:538
DESCRIPTION:The applied pi-calculus is a powerful framework to model proto
cols and to define security properties. In this symbolic model\, it is pos
sible to verify automatically complex security properties such as strong s
ecrecy\, anonymity and unlinkability properties which are based on equival
ence of processes. In this talk\, we will see an overview of a verificatio
n method used by a tool\, Akiss. The tool is able to handle \n\n - a wide
range of cryptographic primitives (in particular AKISS is the only tool ab
le to verify equivalence properties for protocols that use xor)\; \n\n - p
rotocols with else branches (the treatment of disequalities is often compl
icated). \n\nWe will also provide some insights on how interleaving due to
concurrency can be effectively handled.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:One Theorem to Rule Them All: A Unified Translation of LTL into om
ega-Automata - Javier Esparza\, Tecnhische Universität München
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180323T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180323T153000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:554
DESCRIPTION:We present a unified translation of LTL formulas into determin
istic Rabin automata\, limit-deterministic Büchi automata\, and nondeterm
inistic Büchi automata. The translations yield automata of asymptotically
optimal size (double or single exponential\, respectively). All three tra
nslations are derived from one single Master Theorem of purely logical nat
ure. The Master Theorem decomposes the language of a formula into a positi
ve boolean combination of languages that can be translated into omega-auto
mata by elementary means. In particular\, the breakpoint\, Safra\, and ran
king constructions used in other translations are not needed.\n\nJoint wor
k with Jan Kretinsky and Salomon Sickert.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Verified Implementation of the Bounded List Container - Raphaël
Cauderlier\, IRIF - Université Paris Diderot
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180514T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180514T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:572
DESCRIPTION:Standard libraries of programming languages provide efficient
implementations for common data containers. The details of these implement
ations are abstracted away by generic interfaces which are specified in te
rms of well understood mathematical structures such as sets\, multisets\,
sequences\, and partial functions. The intensive use of container librarie
s makes important their formal verification.\n\nI will present a case stud
y of full functional verification of the bounded doubly-linked list contai
ner of from the standard library of Ada 2012. This library is specified in
SPARK and several client programs depend on this specification.\n\nHoweve
r\, the low-level invariants required to verify this library cannot be exp
ressed in SPARK. For this reason\, the proof of functional correctness is
done using VeriFast\, a verification environment for Separation Logic exte
nded with algebraic data types. The specifications proved entail the contr
acts of the Ada library and include new features. The verification method
we used employs a precise algebraic model of the data structure and we sho
w that it facilitates the verification and captures entirely the library c
ontracts.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:RustBelt: Logical Foundations for the Future of Safe Systems Progr
amming - Derek Dreyer\, Max Planck Institute for Software Systems (MPI-SWS
)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180601T103000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180601T113000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:573
DESCRIPTION:Rust is a new systems programming language\, developed at Mozi
lla\, that promises to overcome the seemingly fundamental tradeoff in lang
uage design between high-level safety guarantees and low-level control ove
r resource management. Unfortunately\, none of Rust's safety claims have b
een formally proven\, and there is good reason to question whether they ac
tually hold. Specifically\, Rust employs a strong\, ownership-based type s
ystem\, but then extends the expressive power of this core type system thr
ough libraries that internally use unsafe features.\n\nIn this talk\, I wi
ll present RustBelt (http://plv.mpi-sws.org/rustbelt)\, the first formal (
and machine-checked) safety proof for a language representing a realistic
subset of Rust. Our proof is extensible in the sense that\, for each new R
ust library that uses unsafe features\, we can say what verification condi
tion it must satisfy in order for it to be deemed a safe extension to the
language. We have carried out this verification for some of the most impor
tant libraries that are used throughout the Rust ecosystem.\n\nAfter revie
wing some essential features of the Rust language\, I will describe the hi
gh-level structure of the RustBelt verification and then delve into detail
about the secret weapon that makes RustBelt possible: the Iris framework
for higher-order concurrent separation logic in Coq (http://iris-project.o
rg). I will explain by example how Iris generalizes the expressive power o
f O'Hearn's original concurrent separation logic in ways that are essentia
l for verifying the safety of Rust libraries. I will not assume any prior
familiarity with concurrent separation logic or Rust.\n\nThis is joint wor
k with Ralf Jung\, Jacques-Henri Jourdan\, Robbert Krebbers\, and the rest
of the Iris team.
LOCATION:3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Verifying a Hash Table and Its Iterators in Higher-Order Separatio
n Logic - François Pottier\, INRIA Paris
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180611T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180611T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:579
DESCRIPTION:In this talk\, I describe the specification and proof of an (i
mperative\,\nsequential) hash table implementation. The usual dictionary o
perations\n(insertion\, lookup\, and so on) are supported\, as well as ite
ration via folds\nand iterators. The code is written in OCaml and verified
using higher-order\nseparation logic\, embedded in Coq\, via the CFML too
l and library. This case\nstudy is part of ANR project Vocal\, whose aim i
s to build a verified OCaml\nlibrary of basic data structures. \n\n(This w
ork was presented at CPP 2017.)
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Static Analysis of Multithreaded Recursive Programs Communicating
via Rendez-vous - Adrien Pommellet\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180507T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180507T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:584
DESCRIPTION:We present in this paper a generic framework for the analysis
of multi-threaded programs with recursive procedure calls\, synchronisatio
n by rendez-vous between parallel threads\, and dynamic creation of new th
reads. To this end\, we consider a model called \\emph{Synchronized Dynami
c Pushdown Networks} (SDPNs) that can be seen as a network of pushdown pro
cesses executing synchronized transitions\, spawning new pushdown processe
s\, and performing internal pushdown actions. The reachability problem for
this model is unfortunately undecidable. Therefore\, we tackle this probl
em by introducing an abstraction framework based on Kleene algebras in ord
er to compute an abstraction of the execution paths between two regular se
ts of configurations. We combine an automata theoretic saturation procedur
e with constraint solving in a finite domain. We then apply this framework
to a Counter-Example Guided Abstraction Refinement (CEGAR) scheme\, using
multiple abstractions of increasing complexity and precision.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Distance on timed words and applications - Eugène Asarin\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180618T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180618T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:601
DESCRIPTION:We introduce and study a new (pseudo) metric on timed words ha
ving several advantages: \n\n- it is global: it applies to words having di
fferent number of events\; \n\n- it is realistic and takes into account im
precise observation of timed events\; thus it reflects the fact that the o
rder of events cannot be observed whenever they are very close to each oth
er\; \n\n- it is suitable for quantitative verification of timed systems:
we formulate and solve quantitative model-checking and quantitative monito
ring in terms of the new distance\, with reasonable complexity\;\n\n- it i
s suitable for information-theoretical analysis of timed systems: due to i
ts pre-compactness the quantity of information in bits per time unit can b
e correctly defined and computed.\n\n(Joint work with Nicolas Basset and
Aldric Degorre)
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Deciding the First-Order Theory of an Algebra of Feature Trees wit
h Updates - Nicolas Jeannerod\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180625T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180625T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:610
DESCRIPTION:The CoLiS project aims at applying techniques from deductive p
rogram verification and analysis of tree transformations to the problem of
analyzing shell scripts. The data structure that is manipulated by these
scripts\, namely the file system tree\, is a complex one.\n\nWe plan to us
e feature trees as an abstract representation of file system tree transfor
mations. We thus investigate an extension of these feature trees that incl
udes the update operation\, which expresses that two trees are similar exc
ept in a particular subtree where there might have been changes.\n\nWe sho
w that the first-order theory of this algebra is decidable via a weak quan
tifier elimination procedure which is allowed to swap existential quantifi
ers for universal quantifiers.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Program Invariants - Joël Ouaknine\, MPI-SWS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180613T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180613T160000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:618
DESCRIPTION:Automated invariant generation is a fundamental challenge in p
rogram analysis and verification\, going back many decades\, and remains a
topic of active research. In this talk I'll present a select overview and
survey of work on this problem\, and discuss unexpected connections to ot
her fields including algebraic geometry\, group theory\, and quantum compu
ting. (No previous knowledge of these fields will be assumed.)\n\nThis is
joint work with Ehud Hrushovski\, Amaury Pouly\, and James Worrell.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Costs and Rewards in Priced Timed Automata - Mahsa Shirmohammadi\,
LIS\, CNRS - Univ. Aix-Marseille
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180629T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180629T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:626
DESCRIPTION:We consider Pareto analysis of reachable states of multi-price
d timed automata (MPTA): timed automata equipped with multiple observers t
hat keep track of costs (to be minimised) and rewards (to be maximised) al
ong a computation. Each observer has a constant non-negative derivative wh
ich may depend on the location of the MPTA. We study the Pareto Domination
Problem\, which asks whether it is possible to reach a target location vi
a a run in which the accumulated costs and rewards Pareto dominate a given
objective vector. We show that this problem is undecidable in general\, b
ut decidable for MPTA with at most three observers. For MPTA whose observe
rs are all costs or all rewards\, we show that the Pareto Domination Probl
em is PSPACE-complete. We also consider an epsilon-approximate Pareto Domi
nation Problem that is decidable without restricting the number and types
of observers. We develop connections between MPTA and Diophantine equation
s. Undecidability of the Pareto Domination Problem is shown by reduction f
rom Hilbert's 10th Problem\, while decidability for three observers is sho
wn by a translation to a fragment of arithmetic involving quadratic forms.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Characterizing Asynchronous Message-Passing Models Through Rounds
- Adam Shimi\, IRIT - ENSEEIHT
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180924T111000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180924T121000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:634
DESCRIPTION:One great issue in conceiving and specifying distributed algor
ithms is the sheer number of models\, differing in subtle and often qualit
ative ways: synchrony\, kind of faults\, number of faults... In the contex
t of message-passing\, one solution is to restrict communication to procee
d by round\; A great variety of models can then be captured in the Heard-O
f model\, with predicates on the communication graph at each round. Howev
er\, this raises another issue: how to characterize a given model by such
a predicate? It depends on how to implement rounds in the model. This is s
traightforward in synchronous models\, thanks to the upper bound on commun
ication delay. On the other hand\, asynchronous models allow unbounded mes
sage delays\, which makes the implementation of rounds dependent on the sp
ecific message-passing model.\n\nI will present our formalization of this
characterization for asynchronous models. Specifically\, we introduce Deli
vered collections: the collection of all messages delivered at each round\
, whether late or not. Defining predicates on Delivered collections then a
llows us to capture message-passing models at the same level of abstractio
n than Heard-Of predicates. The question is then reformulated to: what Hea
rd-Of predicates can be generated by a given Delivered predicate?\n\nI wil
l provide an answer by considering all possible scheduling of deliveries o
f messages from the Delivered collections and change of rounds for the pro
cesses. Strategies of processes then constrain those scheduling by specify
ing when processes can change rounds\; those ensuring no process is ever b
locked forever generate a Heard-Of collection per run\, that is a Heard-Of
predicate. Finally\, we use these strategies to nd a characterizing Hear
d-Of predicate through a dominance relation on strategies: a dominant stra
tegy for a Delivered predicate implements the most constrained Heard-Of pr
edicate possible. This approach oer both the dominant Heard-Of predicates
for classical asynchronous models and the existence\, for every Delivered
predicate\, of a strategy dominating large classes of strategies. On the
whole\, those results confirm the power of this formalization and demonstr
ate the characterization of asynchronous models through rounds as a worthw
hile pursuit.\n\nThis is joint work with Aurélie Hurault and Philippe Qu
éinnec.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Regular inference on artificial neural networks - Franz Mayr\, Uni
versidad ORT\, Uruguay
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20180917T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20180917T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:639
DESCRIPTION:This paper explores the general problem of explaining the beha
vior of artificial neural networks (ANN). The goal is to construct a repre
sentation which enhances human understanding of an ANN as a sequence class
ifier\, with the purpose of providing insight on the rationale behind the
classification of a sequence as positive or negative\, but also to enable
performing further analyses\, such as automata-theoretic formal verificati
on. In particular\, a probabilistic algorithm for constructing a determini
stic finite automaton which is approximately correct with respect to an ar
tificial neural network is proposed.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:On Rationality of Nonnegative Matrix Factorization - Mahsa Shirmoh
ammadi\, LIS - CNRS & Université Aix-Marseille
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181001T111000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181001T121000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:652
DESCRIPTION:Nonnegative matrix factorization (NMF) is the problem of decom
posing a given nonnegative n×m matrix M into a product of a nonnegative n
×d matrix W and a nonnegative d×m matrix H. A longstanding open question
\, posed by Cohen and Rothblum in 1993\, is whether a rational matrix M al
ways has an NMF of minimal inner dimension d whose factors W and H are als
o rational. We answer this question negatively\, by exhibiting a matrix fo
r which W and H require irrational entries. \n\nIn this talk\, we further
exhibit a connection between Cohen and Rothblum's question with a question
posed by Paz\, in his seminal 1971 textbook. The latter question asks\,
given a probabilistic automaton (PA) with rational transition probabilitie
s\, does there always exist a minimal equivalent PA that also has rational
transition probabilities? The PA and its minimal equivalent PA accept al
l finite words with equal probabilities. We use the established connection
to answer Paz's question negatively\, thus falsifying a positive answer c
laimed in 1974. (This talk is based on a paper in SODA 2017.)
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:It Is Easy to Be Wise After the Event: Communicating Finite-State
Machines Capture First-Order Logic with "Happened Before" - Marie Fortin\,
LSV - ENS Paris-Saclay
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181022T111000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181022T121000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:663
DESCRIPTION:Message sequence charts (MSCs) naturally arise as executions o
f communicating finite-state machines (CFMs)\, in which finite-state proce
sses exchange messages through unbounded FIFO channels. We study the first
-order logic of MSCs\, featuring Lamport's happened-before relation. We in
troduce a star-free version of propositional dynamic logic (PDL) with loop
and converse. Our main results state that (i) every first-order sentence
can be transformed into an equivalent star-free PDL sentence (and converse
ly)\, and (ii) every star-free PDL sentence can be translated into an equi
valent CFM. This answers an open question and settles the exact relation b
etween CFMs and fragments of monadic second-order logic. As a byproduct\,
we show that first-order logic over MSCs has the three-variable property.\
n\nThis is joint work with Benedikt Bollig and Paul Gastin\, presented at
CONCUR’18.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Replicated Synchronization of BSPlib Programs - Arvid Jakobsson\,
Huawei Research & LIFO -Université d'Orléans
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181112T111000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181112T121000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:666
DESCRIPTION:The BSP model (Bulk Synchronous Parallel) simplifies the const
ruction and evaluation of parallel algorithms\, with its simplified synchr
onization structure and cost model. Nevertheless\, imperative BSP programs
can suffer from synchronization errors. Programs with textually aligned b
arriers are free from such errors\, and this structure eases program compr
ehension. We propose a simplified formalization of barrier inference as da
ta flow analysis\, which verifies statically whether an imperative BSP pro
gram has replicated synchronization\, which is a sufficient condition for
textual barrier alignment.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:The Essence of Gradual Typing - Éric Tanter\, PLEIAD - Universida
d de Chile & INRIA Paris
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181029T111000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181029T121000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:684
DESCRIPTION:Gradual typing enables programming languages to seamlessly com
bine dynamic and static checking. Language researchers and designers have
extended a wide variety of type systems to support gradual typing. These e
fforts consistently demonstrate that designing a satisfactory gradual coun
terpart to a static type system is challenging\, and this challenge only i
ncreases with the sophistication of the type system. Gradual type system d
esigners need more formal tools to help them conceptualize\, structure\, a
nd evaluate their designs.\n\nBased on an understanding of gradual types a
s abstractions of static types\, we have developed systematic foundations
for gradual typing based on abstract interpretation\, called Abstracting G
radual Typing (AGT for short). Gradual languages designed with the AGT app
roach satisfy\, by construction\, the established criteria for gradually-t
yped languages. After a brief introduction to AGT\, this talk reports on o
ur experience applying AGT to various typing disciplines.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Building Reliable Systems on Reliable Foundations - Vincent Rahli\
, SnT - University of Luxembourg
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181203T111000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181203T121000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:685
DESCRIPTION:Current mainstream programming/verification tools are not well
-suited to build safe and secure distributed programs that meet required s
pecifications. This is a serious issue because our modern society came to
heavily rely on complex and constantly evolving distributed systems that n
eed to tolerate all kinds of threats and attacks in order to protect criti
cal and sensitive resources. This issue is due in part to the lack of form
alisms\, tools\, and reliable foundations. Indeed\, in the past few decade
s\, we have seen a spurt of verification tools that handle well functional
sequential code\, but expressive tools to reason about distributed progra
ms are only just emerging. Moreover\, a major issue with such verification
tools is that they are often very complex themselves\, making them error
prone.\n\nIn this talk I will present some of my contributions to this are
a\, namely\, I will present my work on (1) designing formal verification t
ools to reason about complex distributed systems (such as Byzantine fault
tolerant consensus protocols as used in Blockchain technology)\; and (2) o
n ensuring that those verification tools rely on correct foundations.\n\nI
will conclude by showing how I believe distributed systems will have a po
sitive impact on modern foundational/logical frameworks\, and vice versa.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Using Alloy to explore Weak Memory and Transactional Memory - John
Wickerson\, Imperial College London
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190415T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190415T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:686
DESCRIPTION:When reasoning about concurrent programs\, it is tempting to i
magine that each thread executes its instructions in order\, and that writ
es to shared memory instantly become visible to all other threads. Alas\,
this ideal (which is called "sequential consistency") is rarely met. In re
ality\, most processors and compilers allow instructions sometimes to be r
eordered\, and loads from shared memory sometimes to retrieve stale data.
This phenomenon is called "weak memory".\n\nThis talk is about how we can
formalise models of weak memory using a tool called Alloy. Using these for
malisations\, we can then synthesise programs that can distinguish differe
nt models of weak memory. We can also check whether a compiler mapping fro
m one weak memory model to another is correct.\n\nThe main case study in t
his talk describes how we used Alloy to find problems in a prototype imple
mentation of transaction memory being developed by ARM. I will also talk a
bout how similar techniques can be used to check the correctness of softwa
re-to-hardware compilers (or "high-level synthesis" tools).\n\nThis talk i
s based on joint work with Mark Batty\, Nathan Chong\, George Constantinid
es\, and Tyler Sorensen. For further reading\, please see papers that appe
ared in [POPL'17](https://johnwickerson.github.io/papers/memalloy.pdf) and
[PLDI'18](https://johnwickerson.github.io/papers/transactions.pdf).
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Fast Asymptotic and Approximate Consensus in Highly Dynamic Networ
ks - Matthias Függer\, LSV - CNRS & ENS de Cachan
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181126T111000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181126T121000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:692
DESCRIPTION:Agreeing on a common value in a distributed system is a proble
m that lies at the heart of many distributed computing problems and occurs
in several flavors. Unfortunately\, even modest network dynamics already
prohibit solvability of exact consensus\, where agents have to decide on
a single output value that is within the range of the agents' initial valu
es.\n\nFor many problems (distributed control\, clock synchronization\, lo
ad balancing\, ...) it is however sufficient to asymptotically converge to
the same value\, or decide on values not too far from each other. We stud
y solvability of these consensus variants in highly dynamic networks\, pro
vide time complexity results\, and present fast algorithms. We then show h
ow the results on dynamic networks are relevant for classical fault-models
\, such as asynchronous message passing with crashes.\n\nThe talk is on pr
evious and current research with Bernadette Charron-Bost (LIX)\, Thomas No
wak (LRI)\, and Manfred Schwarz (ECS\, TU Wien).
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:On the Complexity of Value Iteration - Mahsa Shirmohammadi\, LIS -
CNRS & Université Aix-Marseille
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181210T111000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181210T121000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:693
DESCRIPTION:Value iteration is a fundamental algorithm for solving Markov
Decision Processes (MDPs). It computes the maximal n-step payoff by iterat
ing n times a recurrence equation which is naturally associated to the MDP
. At the same time\, value iteration provides a policy for the MDP that is
optimal on a given finite horizon n. In this talk\, we settle the computa
tional complexity of value iteration. We show that\, given a horizon n in
binary and an MDP\, computing an optimal policy is EXP-complete\, thus res
olving an open problem that goes back to the seminal 1987 paper on the com
plexity of MDPs by Papadimitriou and Tsitsiklis. As a stepping stone\, we
show that it is EXP-complete to compute the n-fold iteration (with n in bi
nary) of a function given by a straight-line program over the integers wit
h max and + as operators.\n\nA preliminary draft of this work is available
on arXiv:\n\nhttps://arxiv.org/abs/1807.04920v2
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Hierarchical Memory Management for Mutable State - Adrien Guatto\,
IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20181105T111000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20181105T121000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:697
DESCRIPTION:It is well known that modern functional programming languages
are naturally amenable to parallel programming. Achieving efficient parall
elism using functional languages\, however\, remains difficult.\nPerhaps t
he most important reason for this is their lack of support for efficient i
n-place updates\, i.e.\, mutation\, which is important for the implementat
ion of both parallel algorithms and the run-time system services (e.g.\, s
chedulers and synchronization primitives) used to execute them.\n\nIn this
joint work with Sam Westrick\, Ram Raghunathan\, Umut Acar\, and Matthew
Fluet\, we propose techniques for efficient mutation in parallel functiona
l languages. To this end\, we couple the memory manager with the thread sc
heduler to make reading and updating data allocated by nested threads effi
cient. We describe the key algorithms behind our technique\, implement the
m in the MLton Standard ML compiler\, and present an empirical evaluation.
Our experiments show that the approach performs well\, significantly impr
oving efficiency over existing functional language implementations.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:A denotational semantics for weak-memory language concurrency with
modular DRF-SC - Mark Batty\, University of Kent
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190128T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190128T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:703
DESCRIPTION:Concurrent languages provide weak semantics: they admit non-se
quentially-consistent (SC) behaviour to accommodate weak target architectu
res and compiler optimisation. Subtle behaviour and intricate specificatio
ns result\, but two properties help to simplify things -- no thin-air valu
es\, and DRF-SC. In the first\, all values must be computed from constants
or inputs to the program\, rather than conjured up\, for example\, throug
h abuse of speculative execution. In DRF-SC\, programs without data races
are guaranteed SC behaviour. Unfortunately\, existing languages like C/C++
admit thin-air values and DRF-SC results only apply to an unrealistic cla
ss of programs\, excluding systems code and code using concurrency librari
es. We provide a modular semantics that avoids thin-air values and we prov
e a new modular variant of DRF-SC that lifts a key barrier to its usefulne
ss.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Modal Separation Logics and Friends - Stéphane Demri\, LSV - CRNS
& ENS Paris Saclay
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190211T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190211T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:726
DESCRIPTION:Separation logic is known as an assertion language to perform
verification\, by extending Hoare-Floyd logic in order to verify programs
with mutable data structures. The separating conjunction allows us to eval
uate formulae in subheaps\, and this possibility to evaluate formulae in a
lternative models is a feature shared with many modal logics such as sabot
age logics\, logics of public announcements or relation-changing modal log
ics. In the first part of the talk\, we present several versions of modal
separation logics whose models are memory states from separation logic and
the logical connectives include modal operators as well as separating con
junction. Fragments are genuine modal logics whereas some others capture s
tandard separation logics\, leading to an original language to speak about
memory states. In the second part of the talk\, we present the decidabili
ty status and the computational complexity of several modal separation log
ics\, (for instance\, leading to NP-complete or Tower-complete satisfiabil
ity problems). In the third part\, we investigate the complexity of fragme
nts of quantified CTL under the tree semantics (or similar modal logics wi
th propositional quantification)\, some of these fragments being related t
o modal separation logics. Part of the presented work is done jointly with
B. Bednarczyk (U. of Wroclaw) or with R. Fervari (U. of Cordoba).
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Time Credits and Time Receipts in Iris - Glen Mével\, INRIA Paris
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190318T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190318T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:764
DESCRIPTION:I present a machine-checked extension of the program logic Iri
s with time credits and time receipts\, two dual means of reasoning about
time. Whereas time credits are used to establish an upper bound on a progr
am’s execution time\, time receipts can be used to establish a lower bou
nd. More strikingly\, time receipts can be used to prove that certain unde
sirable events—such as integer overflows—cannot occur until a very lon
g time has elapsed. I will present a simple machine-checked application of
time receipts\, and sketch how we define our extension of Iris (and prove
its soundness) in a modular way\, as a layer above Iris.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:A proof framework for mobile robots protocols - Pierre Courtieu\,
CNAM
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190225T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190225T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:768
DESCRIPTION:Distributed algorithms are known to be very difficult to desig
n and certify. If these algorithms need to be fault or byzantine resilient
the difficulty is even greater. Examples of flawed algorithms and proofs
are numerous. It is therefore a natural domain for mechanized proofs (i.e.
with the help of a proof assistant): the additional work of mechanizing t
he proofs should be worth the effort.\n\nWe present a framework\, named Pa
ctole\, for designing distributed protocols for mobile robots\, stating pr
operties about these protocols and proving these properties. We can also p
rove *impossibility statement* i.e. that there exists no protocol achievin
g some property.\n\nOur technique cannot be compared to but can be seen as
complementary to model checking in the sense that our proofs are not auto
mated but allow for instance to conclude that a protocol is correct *for a
ny* starting configuration\, number of robots\, that is not proven impossi
ble.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Parameter Synthesis for Extended Signal Temporal Logic Specificati
ons - José Ignacio Requeno\, Université Grenoble Alpes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190218T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190218T150000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:784
DESCRIPTION:Cyber-Physical Systems (CPS) are complex environments composed
of embedded computers that monitor or control physical processes. Nowaday
s\, they are ubiquitously present in most aspects of our live\, ranging fr
om power stations to communications\, transport or finances. Guaranteeing
a correct behaviour and a good quality of service (QoS) of such critical s
ystems is imperative. Signal temporal logic (STL) is a specification langu
age that is adapted for dealing with continuous time real-value properties
which are characteristic in CPSs. Used in combination with formal models
and model checking techniques\, it allows the verification and validation
of runtime executions. In this talk\, I will present recent improvements i
n the STL language\; including a new method for inferring the validity dom
ain of parametric STL specifications.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Invariant safety for distributed applications - Sreeja Nair\, LIP
6 - Sorbonne Université
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190315T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190315T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:789
DESCRIPTION:A distributed application replicates data closer to the user t
o ensure shorter response times and availability when the network partitio
ns. The replicas should be able to allow updates even in case of network p
artitions and they send their states to converge. The application develope
r must also make sure that the application invariants hold true even when
the replicas diverge.\n\nIn this talk\, we present a proof methodology for
verifying the safety of invariants of highly-available distributed applic
ations that replicate state. The proof is modular and sequential :one can
reason about each individual operation separately\, and one can reason abo
ut a distributed application as if it were sequential. We automate the met
hodology and illustrate the use of the tool with a representative example.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Get rid of inline assembly through trustable verification-oriented
lifting - Richard Bonichon\, CEA List
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190311T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190311T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:793
DESCRIPTION:Formal methods for software development have made great stride
s in the last two decades\, to the point that their application in safety-
critical embedded software is an undeniable success. Their extension to no
n-critical software is one of the notable forthcoming challenges. For exam
ple\, C programmers regularly use inline assembly for low-level optimizati
ons and system primitives. This usually results in driving state-of-the-ar
t formal analyzers developed for C ineffective. We thus propose TInA\, an
automated\, generic\, trustworthy and verification-oriented lifting techni
que turning inline assembly into semantically equivalent C code\, in order
to take advantage of existing C analyzers. Extensive experiments on real-
world C code with inline assembly (including GMP and ffmpeg) show the feas
ibility and benefits of TInA.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Beyond admissibility: Dominance between chains of strategies - Mar
ie Van Den Boogard\, Université Libre de Bruxelles
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190304T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190304T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:794
DESCRIPTION:In this talk\, we focus on the concept of rational behaviour i
n multi-player games on finite graphs\, taking the point of view of a play
er that has access to the structure of the game but cannot make assumption
s on the preferences of the other players. In the qualitative setting\, ad
missible strategies have been shown to fit the rationality requirements\,
as they coincide with winning strategies when these exist\, and enjoy the
fundamental property that every strategy is either admissible or dominated
by an admissible strategy. However\, as soon as there are three or more p
ayoffs\, one finds that this fundamental property does not necessarily hol
d anymore: one may observe chains of strategies that are ordered by domina
nce and such that no admissible strategy dominates any of them. Thus\, to
recover a satisfactory rationality notion (still based on dominance)\, we
depart from the single strategy analysis approach and consider instead cha
ins of strategies as families of behaviours. We establish a sufficient cri
terion for games to enjoy a similar fundamental property\, ie\, all chains
are below some maximal chain\, and\, as an illustration\, we present a cl
ass of games where admissibility fails to capture some intuitively rationa
l behaviours\, while our chain-based analysis does. Based on a joint work
with N.Basset\, I. Jecker\, A. Pauly and J.-F. Raskin\, presented at CSL'1
8.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Automated Hypersafety Verification - Azadeh Farzan\, University of
Toronto
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190305T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190305T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:810
DESCRIPTION:In this talk\, I will introduce an automated verification tech
nique for hypersafety properties\, which express sets of valid interrelati
ons between multiple finite runs of a program. They can alternatively be v
iewed as standard safety properties of a product of the several copies of
the program by itself. The key observation is that a small representative
set of the product program runs\, called a reduction\, is sufficient to co
nstruct a formal proof. I will present an algorithm based on a counterexam
ple-guided refinement loop that simultaneously searches for a reduction an
d a proof of the correctness for the reduction. The algorithm is implement
ed in a tool and there is evidence that itl is very effective in verifying
a diverse array of hypersafety properties for a diverse class of input pr
ograms.
LOCATION:3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Safe Deferred Memory Reclamation with Types - Ismail Kuru\, Drexel
University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190411T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190411T150000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:822
DESCRIPTION:Memory management in lock-free data structures remains a major
challenge in concurrent programming. Design techniques including read-cop
y-update (RCU) and hazard pointers provide workable solutions\, and are wi
dely used to great effect. These techniques rely on the concept of a grace
period: nodes that should be freed are not deallocated immediately\, and
all threads obey a protocol to ensure that the deallocating thread can det
ect when all possible readers have completed their use of the object. This
provides an approach to safe deallocation\, but only when these subtle pr
otocols are implemented correctly. We present a static type system to ensu
re correct use of RCU memory management: that nodes removed from a data st
ructure are always scheduled for subsequent deallocation\, and that nodes
are scheduled for deallocation at most once. As part of our soundness proo
f\, we give an abstract semantics for RCU memory management primitives whi
ch captures the fundamental properties of RCU. Our type system allows us t
o give the first proofs of memory safety for RCU linked list and binary se
arch tree implementations without requiring full verification.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Shared Objects in Distributed Systems: A Broadcast Perspective - M
atthieu Perrin\, Université de Nantes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190506T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190506T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:855
DESCRIPTION:It is well-known that consensus (one-set agreement) and total
order broadcast are equivalent in asynchronous systems prone to process cr
ash failures. Considering wait-free systems\, this talk addresses and answ
ers the following question: which are the communication abstraction that
“captures”\, on the one hand\, read/write registers\, and on the other
hand\, k-set agreement?\n\nTo this end\, it introduces a new broadcast co
mmunication abstraction\, called k-SCD-Broadcast\, which restricts the dis
agreement on the local deliveries of the messages that have been broadcast
: 1-SCD-Broadcast boils down to total order broadcast and n-SCD-Broadcast
is equivalent to the read/write register. Hence\, in this context\, k = 1
is not a special number\, but only the first integer in an increasing inte
ger sequence. This establishes a new “correspondence” between distribu
ted agreement problems and communication abstractions\, which enriches our
understanding of the relations linking fundamental issues of fault-tolera
nt distributed computing.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:On the self in Selfie - Cristoph Kirsch\, Universität Salzburg
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190405T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190405T153000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:856
DESCRIPTION:Selfie is a self-contained 64-bit\, 10-KLOC implementation of
(1) a self-compiling compiler written in a tiny subset of C called C* targ
eting a tiny subset of 64-bit RISC-V called RISC-U\, (2) a self-executing
RISC-U emulator\, (3) a self-hosting hypervisor that virtualizes the emula
ted RISC-U machine\, and (4) a prototypical symbolic execution engine that
executes RISC-U symbolically. Selfie can compile\, execute\, and virtuali
ze itself any number of times in a\nsingle invocation of the system given
adequate resources. There is also a simple linker\, disassembler\, debugge
r\, and profiler. C* supports only two data types\, uint64_t and uint64_t*
\, and RISC-U features just 14 instructions\, in particular for unsigned a
rithmetic only\, which significantly simplifies reasoning about correctnes
s. Selfie has originally been developed just for educational purposes but
has by now become a research platform as well. We discuss\nhow selfie leve
rages the synergy of integrating compiler\, target machine\, and hyperviso
r in one self-referential package while orthogonalizing bootstrapping\, vi
rtual and heap memory management\, emulated and virtualized concurrency\,
and even replay debugging and symbolic execution.\n\nThis is joint work wi
th Alireza S. Abyaneh\, Simon Bauer\, Philipp Mayer\, Christian Mösl\, Cl
ément Poncelet\, Sara Seidl\, Ana Sokolova\, and Manuel Widmoser\, Univer
sity of Salzburg\, Austria\n\n\nWeb:\n\nhttp://selfie.cs.uni-salzburg.at
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Design\, Verification and Automatic Implementation of Correct-by-C
onstruction Distributed Transaction Systems in Maude - Si Liu\, University
of Illinois at Urbana-Champaign
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190416T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190416T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:861
DESCRIPTION:Designing\, verifying\, and implementing highly reliable distr
ibuted systems is at present a hard and very labor-intensive task. Cloud-b
ased systems have further increased this complexity due to the desired con
sistency\, availability\, scalability\, and disaster tolerance. This talk
addresses this challenge in the context of distributed transaction systems
(DTSs) from two complementary perspectives: (i) designing DTSs in Maude w
ith high assurance such that they satisfy desired correctness and performa
nce requirements\; and (ii) transforming verified Maude designs of DTSs in
to correct-by-construction distributed implementations. Regarding (i)\, I
will talk about our Maude-based framework for automatic analysis of consis
tency and performance properties of DTSs. Regarding (ii)\, I will present
a correct-by-construction automatic transformation mapping a verified form
al specification of an actor-based distributed system design in Maude to a
distributed implementation enjoying the same safety and liveness properti
es as the original formal design.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Lesson on Timed Automata Reachability - Mahsa Shirmohammadi\, LI
S - CNRS & Univ. Aix-Marseille
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190510T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190510T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:864
DESCRIPTION:Advertisement:\n \nThe old-standing\, natural\, and useful
problem of characterizing the reachability relation for timed automata ha
s been solved many times: by Hubert Comon and Yan Jurski\, by Catalin Dima
\, by Pavol Krcal\, etc. Still all these characterizations are difficult t
o understand and to use in practise. Recently\, Mahsa Shirmohammadi and Be
n Worrell came up with a new solution\, anod moreover they say that it is
very easy! Mahsa will present it in the form of a black-(or white-)board l
esson on May 10th\, from 11-13hs.\n\nAbstract:\n\nIn our preprint (submitt
ed to IPL)[*]\, we give a simple and short proof of effective definability
of the reachability relation in timed automata. We use a small trick that
reduces this problem to that of computing the set of configurations reach
able from a fixed initial configuration in timed automata. The proof uses
only Parikh theorem in heart and 1-bounded region automata\, so to follow
the proof one may not need any prior knowledge of timed automata.\n\n[*] h
ttps://arxiv.org/abs/1903.09773
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Functional Verification of Tezos Smart Contracts in Coq - Raphaël
Cauderlier\, Nomadic Labs
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190520T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190520T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:865
DESCRIPTION:Smart contract blockchains such as Ethereum and Tezos let thei
r users program their crypto-money accounts. Bugs in these smart contracts
can lead to huge losses. Yet smart contracts are necessarily small progra
ms because checking the blockchain requires to evaluate all the smart cont
ract calls in the history of the chain. For these reasons\, smart contract
languages are a good spot for formal methods.\n\nThe Tezos blockchain and
its smart contract language Michelson have been designed with verificatio
n in mind. In this talk\, I will present Mi-Cho-Coq\, a formal specificati
on of Michelson in the Coq proof assistant. I will also demonstrate how to
use it for functional verification of a typical multisig smart contract.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:From MapReduce to Apache Beam: A Journey in Abstraction - Pierre-M
alo Deniélou\, Google
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190617T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190617T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:869
DESCRIPTION:Processing large amounts of data used to be an affair of speci
alists: specialized hardware\, specialized software\, specialized programm
ing model\, specialized engineers. MapReduce was the first widely adopted
high-level API for large-scale data processing. It helped democratize big
data processing by providing a clear abstraction that was supported by sev
eral efficient systems. \n\nIn this talk\, I will present how the programm
ing APIs (and underlying systems) for large-scale data processing evolved
in the past 20 years\, both within Google and in the open source world. I
will start from MapReduce and Millwheel and finish with Apache Beam and wh
ere we're headed next.\n\n(*) This will be a joint session of the Système
s Complexes\, Vérification and PPS seminars
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Randomized Testing of Distributed Systems with Probabilistic Guara
ntees - Burcu Külahçıoğlu Özkan\, Max Planck Institute for Software S
ystems (MPI-SWS)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190611T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190611T160000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:892
DESCRIPTION:Several recently proposed randomized testing tools for concurr
ent and distributed systems come with theoretical guarantees on their succ
ess. The key to these guarantees is a notion of bug depth—the minimum le
ngth of a sequence of events sufficient to expose the bug—and a characte
rization of d-hitting families of schedules—a set of schedules guarantee
d to cover every bug of given depth d. Previous results show that in certa
in cases the size of a d-hitting family can be significantly smaller than
the total number of possible schedules. However\, these results either ass
ume shared-memory multithreading\, or that the underlying partial ordering
of events is known statically and has special structure. These assumption
s are not met by distributed message-passing applications.\n\nIn this talk
\, we present a randomized scheduling algorithm for testing distributed sy
stems. In contrast to previous approaches\, our algorithm works for arbitr
ary partially ordered sets of events revealed online as the program is bei
ng executed. We show that for partial orders of width at most w and size a
t most n (both statically unknown)\, our algorithm is guaranteed to sample
from at most w^2.n^(d−1) schedules\, for every fixed bug depth d. Thus\
, our algorithm discovers a bug of depth d with probability at least 1/ (w
^2.n^(d−1)). As a special case\, our algorithm recovers a previous rando
mized testing algorithm for multithreaded programs. Our algorithm is simpl
e to implement\, but the correctness arguments depend on difficult combina
torial results about online dimension and online chain partitioning of par
tially ordered sets.\nIn the last part of the talk\, we briefly discuss ho
w we can exploit state-space reduction strategies from model checking to p
rovide better guarantees for the probability of hitting bugs. This will mo
ve us towards a randomized algorithm which brings together two orthogonal
reductions of the search space: depth-bounded testing and dependency-aware
testing.\n\n(Joint work with Rupak Majumdar\, Filip Niksic\, Simin Oraee\
, Mitra Tabaei Befrouei\, Georg Weissenbacher)
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:The complexity of some easy subclasses of the Skolem problem - Nik
hil Balaji\, University of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190701T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190701T150000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:904
DESCRIPTION:Given a linear recurrence sequence (LRS)\, is there an algorit
hm that decides if the infinite sequence of numbers generated by the LRS c
ontains 0? This is the notorious Skolem problem. The Skolem-Mahler-Lech th
eorem says that the set of zeros of an LRS is semi-linear\; however\, this
doesn't translate to an algorithm\, due to lack of effective bounds on th
e description of the zero set.\n\nThis algorithmic question has remained o
pen despite several decades of active research\, with decidability known o
nly for a few restricted subclasses\, by either restricting the depth of t
he LRS (up to 4) or by restricting the structure of the LRS (especially ro
ots of the characteristic polynomials). Recent work due to Ouaknine and Wo
rrell has shown that decidability of closely related algorithmic questions
could entail significant breakthroughs in Diophantine approximation.\n\nI
n this talk\, we first present an elementary proof that this problem is NP
-hard (which was already observed by Blondel and Portier). We further stud
y some easy subclasses which are known to be decidable from the point of v
iew of proving better complexity upper bounds. We are able to show that fo
r a wide class of special cases of LRS\, the zero set has efficiently veri
fiable certificates.\n\nBased on joint ongoing work with S. Akshay\, Anike
t Muhrekar\, Rohith Varma and Nikhil Vyas.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Büchi Objectives in Countable MDPs - Mahsa Shirmohammadi\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190705T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190705T153000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:912
DESCRIPTION:We study countably infinite Markov decision processes with Bü
chi objectives\, which ask to visit a given subset of states infinitely of
ten. A question left open by T.P. Hill in 1979 is whether there always exi
st ε-optimal Markov strategies\, i.e.\, strategies that base decisions on
ly on the current state and the number of steps taken so far. We provide a
negative answer to this question by constructing a non-trivial counterexa
mple. On the other hand\, we show that Markov strategies with only 1 bit o
f extra memory are sufficient. This work is in collaboration with Stefan K
iefer\, Richard Mayr and Patrick Totzke\, and is going to be presented in
ICALP 2019. A full version is at https://arxiv.org/abs/1904.11573
LOCATION:Salle 1001
END:VEVENT
BEGIN:VEVENT
SUMMARY:Selective monitoring - Stefan Kiefer\, University of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190923T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190923T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:921
DESCRIPTION:We study selective monitors for labelled Markov chains. Monito
rs observe the outputs that are generated by a Markov chain during its run
\, with the goal of identifying runs as correct or faulty. A monitor is se
lective if it skips observations in order to reduce monitoring overhead. W
e are interested in monitors that minimize the expected number of observat
ions. We establish an undecidability result for selectively monitoring gen
eral Markov chains. On the other hand\, we show for non-hidden Markov chai
ns (where any output identifies the state the Markov chain is in) that sim
ple optimal monitors exist and can be computed efficiently\, based on DFA
language equivalence. These monitors do not depend on the precise transiti
on probabilities in the Markov chain. We report on experiments where we co
mpute these monitors for several open-source Java projects.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:The Complexity of Flat Freeze LTL - Arnaud Sangnier\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191118T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191118T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:923
DESCRIPTION:We consider the model-checking problem for freeze LTL on one-c
ounter automata (OCAs). Freeze LTL extends LTL with the freeze quantifier\
, which allows one to store different counter values of a run in registers
so that they can be compared with one another. As the model-checking prob
lem is undecidable in general\, we focus on the flat fragment of freeze LT
L\, in which the usage of the freeze quantifier is restricted. Recently\,
Lechner et al. showed that model checking for flat freeze LTL on OCAs with
binary encoding of counter updates is decidable and in 2NEXPTIME. In this
paper\, we prove that the problem is\, in fact\, NEXPTIME-complete no mat
ter whether counter updates are encoded in unary or binary. Like Lechner e
t al.\, we rely on a reduction to the reachability problem in OCAs with pa
rameterized tests (OCAPs). The new aspect is that we simulate OCAPs by alt
ernating two-way automata over words. This implies an exponential upper bo
und on the parameter values that we exploit towards an NP algorithm for re
achability in OCAPs with unary updates. We obtain our main result as a cor
ollary.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:On Solving String Constraints - Mohamed Faouzi Atig\, Uppsala Univ
ersity
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191021T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191021T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:924
DESCRIPTION:String data types are present in all conventional programming
and scripting languages. In fact\, it is almost impossible to reason about
the correctness and security of such programs without having a decision p
rocedure for string constraints. A typical string constraint consists of w
ord equations over string variables denoting strings of arbitrary lengths\
, together with constraints on (i) the length of strings\, and (ii) the re
gular languages to which strings belong. Decidability of this general logi
c is still open.\nIn this talk\, we will discuss recent results on the dec
idability and decision procedures for string constraints. We will focus on
decision procedures that are sound and complete for a well-defined fragme
nt of string constraints. We will also cover a technique that uses a Count
er-Example Guided Abstraction Refinement (CEGAR) framework which contains
both an under- and an over-approximation module. The flow of information b
etween these modules allows increasing the precision in an automatic manne
r.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Expected Finite Horizon - Laurent Doyen\, LSV\, ENS Paris-Saclay
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191014T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191014T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:925
DESCRIPTION:A classical problem in discrete planning is to consider a weig
hted graph and construct a path that maximizes the sum of weights for a gi
ven time horizon T. However\, in many scenarios\, the time horizon is not
fixed\, but the stopping time is chosen according to some distribution suc
h that the expected stopping time is T. If the stopping time distribution
is not known\, then to ensure robustness\, the distribution is chosen by a
n adversary\, to represent the worst-case scenario.\n\nA stationary plan f
or every vertex always chooses the same outgoing edge. For fixed horizon T
\, stationary plans are not sufficient for optimality. Quite surprisingly
we show that when an adversary chooses the stopping time distribution with
expected stopping time T\, then stationary plans are sufficient. While co
mputing optimal stationary plans for fixed horizon is NP-complete\, we sho
w that computing optimal stationary plans under adversarial stopping time
distribution can be achieved in polynomial time. Consequently\, our polyno
mial-time algorithm for adversarial stopping time also computes an optimal
plan among all possible plans.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Deciding language inclusion problems using quasiorders - Pierre Ga
nty\, IMDEA Software Institute
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191028T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191028T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:929
DESCRIPTION:We study the language inclusion problem L1 ⊆ L2 where L1 is
regular or\ncontext-free. Our approach checks whether an overapproximation
of L1 is\nincluded in L2. Such overapproximations are obtained using quas
iorder relations\non words where the abstraction gives the language of all
words “greater than or\nequal to” a given input word for that quasior
der. We put forward a range of\nquasiorders that allow us to systematicall
y design decision procedures for\ndifferent language inclusion problems su
ch as context-free languages into\nregular languages and regular languages
into trace sets of one-counter nets.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:On the complexity of linear arithmetic theories over the integers
- Dmitry Chistikov\, University of Warwick
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191129T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191129T153000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:930
DESCRIPTION:Given a system of linear Diophantine equations\, how difficult
is it to\ndetermine whether it has a solution? What changes if equations
are replaced\nwith inequalities? If some of the variables are quantified u
niversally?\nThese and similar questions relate to the computational compl
exity of deciding\nthe truth value of statements in various logics. This i
ncludes in particular\nPresburger arithmetic\, the first-order logic over
the integers with addition\nand order.\n\nIn this talk\, I will survey con
structions and ideas that underlie known\nanswers to these questions\, fro
m classical results to recent developments\,\nand open problems.\n\nFirst\
, we will recall the geometry of integer linear programming and how it\nin
teracts with quantifiers. This will take us from classical results\ndue to
von zur Gathen and Sieveking (1978)\, Papadimitriou (1981)\, and others\n
to the geometry of the set of models of quantified logical formulas. We wi
ll\nlook at rational convex polyhedra and their discrete analogue\, hybrid
linear\nsets (joint work with Haase (2017))\, and see\, in particular\, h
ow the latter\nform a proper sub-family of ultimately periodic sets of int
eger points in\nseveral dimensions (the semi-linear sets\, introduced by P
arikh (1961)).\n\nSecond\, we will discuss "sources of hardness": which as
pects of the expressive\npower make decision problems for logics over the
integers hard. Addition and\nmultiplication combined enable simulation of
arbitrary Turing machines\, and\nrestriction of multiplication to bounded
integers corresponds to\nresource-bounded Turing machines. How big can the
se bounded integers be in\nPresburger arithmetic? This leads to the proble
m of representing big numbers\nwith small logical formulae\, and we will s
ee constructions by Fischer and\nRabin (1974) and by Haase (2014). We will
also look at the new "route" for\nexpressing arithmetic progressions (in
the presence of quantifier alternation)\nvia continued fractions\, recentl
y discovered by Nguyen and Pak (2017).
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:The Infer Static Analysis platform - Jules Villard\, Facebook
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191216T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191216T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:932
DESCRIPTION:Infer is an open-source static analysis platform for Java\, C\
, C++\, and\nObjective-C. Infer is deployed at several companies where it
helps\ndevelopers write better code.\n\nThis talk will present how Infer i
s used at Facebook\, where it analyses\nthousands of code changes every mo
nth\, leading to thousands of bugs\nbeing found and fixed before they reac
h users. We will then see how to\nwrite your own inter-procedural static a
nalysis in just a few lines of\ncode inside Infer\, and automatically be a
ble to apply it to millions of\nlines of code.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Timed Basic Parallel Processes - Patrick Totzke\, Liverpool Univer
sity
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191115T143000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191115T153000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:940
DESCRIPTION:I will talk about two fun constructions for reachability analy
sis of one-clock\ntimed automata\, which lead to concise logical character
izations in existential\nLinear Arithmetic.\n\nThe first one describes "pu
nctual" reachability relations: reachability in\nexact time t. It uses a c
oarse interval abstraction and counting of resets via\nParikh-Automata.\nT
he other is a "sweep line" construction to compute optimal time to reach i
n\nreachability games played on one-clock TA.\n\nTogether\, these can be u
sed to derive a (tight) NP complexity upper bound for\nthe coverability an
d reachability problems in an interesting subclass of Timed\nPetri Nets\,
which naturally lends itself to parametrised safety checking of\nconcurren
t\, real-time systems. This contrasts with known super-Ackermannian\ncompl
eteness\, and undecidability results for unrestricted Timed Petri nets.\n\
nThis is joint work with Lorenzo Clemente and Piotr Hofman\, and was prese
nted at\nCONCUR'19. Full details are available at https://arxiv.org/abs/19
07.01240.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Deductive Proof of Industrial Smart Contracts Using Why3 - Zeinab
Nehaï\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191104T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191104T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:951
DESCRIPTION:A bug or error is a common problem that any software or comput
er program may encounter. It can occur from badly writing the program\, a
typing error or bad memory management. However\, errors can become a signi
ficant issue if the unsafe program is used for critical systems. Therefore
\, the use of formal methods for this kind of systems is greatly required.
In this work\, we apply a formal method that performs deductive verificat
ion on industrial smart contracts\, which are self-executing\ndigital prog
rams. Because smart contracts manipulate cryptocurrency and transaction in
formation\, if a bug occurs in such programs\, serious consequences can ha
ppen\, such as a loss of money. The aim of this work is to show that a lan
guage dedicated to deductive verification\, called Why3\, can be a suitabl
e language to write correct and proven contracts.\nWe first encode existin
g contracts into the Why3 program\; next\, we formulate specifications to
be proved as the absence of RunTime Error and functional properties\, then
we verify the behaviour of the program using the Why3 system. Finally\, w
e compile the Why3 contracts to the Ethereum Virtual Machine (EVM). Moreov
er\, our approach estimates the cost of gas\, which is a unit that measure
s the amount of computational effort during a transaction.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Checking Robustness Against Snapshot Isolation - Sidi Mohamed Beil
lahi\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191209T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191209T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:952
DESCRIPTION:Transactional access to databases is an important abstraction
allowing programmers to consider blocks of actions (transactions) as execu
ting in isolation. \nThe strongest consistency model is serializability\,
which ensures the atomicity abstraction of transactions executing over a s
equentially consistent memory. \nSince ensuring serializability carries a
significant penalty on availability\, modern databases provide weaker cons
istency models\, one of the most prominent being snapshot isolation. \nIn
general\, the correctness of a program relying on serializable transaction
s may be broken when using weaker models. However\, certain programs may a
lso be insensitive to consistency relaxations\, i.e.\, all their propertie
s holding under serializability are preserved even when they are executed
over a weak consistent database and without additional synchronization.\n\
nIn this talk\, we address the issue of verifying if a given program is ro
bust against snapshot isolation\, i.e.\, all its behaviors are serializabl
e even if it is executed over a database ensuring snapshot isolation. We s
how that this verification problem is polynomial time reducible to a state
reachability problem in transactional programs over a sequentially consis
tent shared memory. This reduction opens the door to the reuse of \nthe cl
assic verification technology for reasoning about sequentially-consistent
programs. In particular\, we show that it can be used to derive a proof te
chnique based on Lipton's reduction theory that allows to prove programs r
obust.\n\nThis is a joint work with Ahmed Bouajjani and Constantin Enea.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:TBA - Corto Mascle\, ENS Paris-Saclay
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20190225T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20190225T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:954
DESCRIPTION:
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Mergeable Replicated Data Types - Suresh Jagannathan\, Purdue Univ
ersity
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191129T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191129T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1012
DESCRIPTION:Programming geo-replicated distributed systems is challenging
given the complexity of reasoning about different evolving states on diffe
rent replicas. Existing approaches to this problem impose a significant b
urden on application developers to consider the effect of how operations p
erformed on one replica are witnessed and applied to others. To alleviate
these challenges\, we present a fundamentally different approach to progr
amming in the presence of replicated state. Our insight is based on the u
se of invertible relational specifications of an inductively-defined data
type as a mechanism to capture salient aspects of the data type relevant t
o how its different instances can be safely merged in a replicated environ
ment. Importantly\, because these specifications only address a data type
's (static) structural properties\, their formulation does not require exp
osing low-level system-level details concerning asynchrony\, replication\,
visibility\,\netc. As a consequence\, our framework enables the correct-
by-construction synthesis of rich merge functions over arbitrarily complex
(i.e.\, composable) data types. Furthermore\, the specification language
allows us to extract sufficient conditions to automatically derive merge
functions with meaningful convergence properties. We have implemented our
ideas in a tool called Quark and have been able to demonstrate the utilit
y of our model on a number of real-world benchmarks.\n\nThis is joint work
with Gowtham Kaki\, Swarn Priya\, and KC Sivaramakrishnan.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Complexity and Information in Invariant Inference - Yotam Feldman\
, Tel Aviv University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191211T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191211T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1025
DESCRIPTION:This work addresses the complexity of SAT-based invariant infe
rence\, a prominent approach to safety verification. \nWe consider the pr
oblem of inferring an inductive invariant of polynomial length given a tra
nsition system and a safety property. \nWe analyze the complexity of this
problem in a black-box model\, called the Hoare-query model\, which is ge
neral enough to capture algorithms such as IC3/PDR and its variants. \nAn
algorithm in this model learns about the system's reachable states by que
rying the validity of Hoare triples. \n \nWe show that in general an alg
orithm in the Hoare-query model requires an exponential number of queries.
Our lower bound is information-theoretic and applies even to computationa
lly unrestricted algorithms\, showing that no choice of generalization fro
m the partial information obtained in a polynomial number of Hoare queries
can lead to an efficient invariant inference procedure in this class. \n
\nWe then show\, for the first time\, that by utilizing rich Hoare queri
es\, as done in PDR\, inference can be exponentially more efficient than a
pproaches such as ICE learning\, which only utilize inductiveness checks o
f candidates. \nWe do so by constructing a class of transition systems fo
r which a simple version of PDR with a single frame infers invariants in a
polynomial number of queries\, whereas every algorithm using only inducti
veness checks and counterexamples requires an exponential number of querie
s. \n \nOur results also shed light on connections and differences with
the classical theory of exact concept learning with queries\, and imply th
at learning from counterexamples to induction is harder than classical exa
ct learning from labeled examples. This demonstrates that the convergence
rate of Counterexample-Guided Inductive Synthesis depends on the form of \
ncounterexamples.\n\nJoint work with Neil Immerman\, Mooly Sagiv\, and Sha
ron Shoham\, that will appear in POPL'20.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Termination of linear constraint loops - James Worrell\, Universit
y of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200224T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200224T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1027
DESCRIPTION:We consider the problem of deciding termination of linear cons
traint loops\, that is\, single-path loops in which the loop body consists
of a (possibly non-deterministic) assignment\, specified a conjunction of
linear constraints. We present several versions of this problem\, accord
ing to the syntactic form of the loop and the numerical domain of the prog
ram variables. We sketch some decidability results and point out open prob
lems.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:On Finite Monoids over Nonnegative Integer Matrices and Short Kill
ing Words - Corto Mascle\, ENS de Cachan
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200217T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200217T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1028
DESCRIPTION:Unambiguous automata are a popular compromise between \nnon-de
terministic and deterministic automata in terms of succinctness \nand comp
lexity. A word is called a killing word for an automaton if \nthere is no
path labelled by it in this automaton. Here we will \ndiscuss the problem
of computing a short killing word for an \nunambiguous automaton\, as well
as possible extensions. Unambiguous \nautomata are closely related to cod
es\, and this problem can be viewed \nas a particular instance of Restivo'
s conjecture\, a longstanding \nproblem in the theory of codes. It can als
o be interpreted as a \nrestricted version of the matrix mortality problem
. This is a joint \nwork with Stefan Kiefer\, published at STACS 2019.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:On the hardness of robust classification - Pascale Gourdeau\, Univ
ersity of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200302T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200302T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1029
DESCRIPTION:It is becoming increasingly important to understand the vulner
ability of machine learning models to adversarial attacks. In this talk\,
we will study the feasibility of robust learning from the perspective of c
omputational learning theory\, considering both sample and computational c
omplexity. In particular\, our definition of robust learnability requires
polynomial sample complexity. We start with two negative results. We show
that no non-trivial concept class can be robustly learned in the distribut
ion-free setting against an adversary who can perturb just a single input
bit. We show moreover that the class of monotone conjunctions cannot be ro
bustly learned under the uniform distribution against an adversary who can
perturb ω(log n) input bits. However if the adversary is restricted to p
erturbingO(log n) bits\, then the class of monotone conjunctions can be ro
bustly learned with respect to a general class of distributions (that incl
udes the uniform distribution). Finally\, we provide a simple proof of the
computational hardness of robust learning on the boolean hypercube. Unlik
e previous results of this nature\, our result does not rely on another co
mputational model (e.g. the statistical query model) nor on any hardness a
ssumption other than the existence of a hard learning problem in the PAC f
ramework.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:"Easy" vs hard analysis for caching policies - David Monniaux\, Un
iversity of Grenoble.
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200210T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200210T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1030
DESCRIPTION:Processors cache data to avoid slow access to main memory. Whe
n a cache set is full\, one block of data is evicted to make room for new
data. A replacement policy chooses which block to evict. The most natural
one is to evict the least recently used (LRU) block. It however had the re
putation among hardware designers of being hard to implement\, and thus th
ey proposed some "pseudo LRU" policies supposed to behave "similarly". The
re is also a FIFO policy\, also easy to implement.\n\nFor safety critical
systems it is sometimes necessary to prove bounds on the worst-case execut
ion time by static analysis. This analysis has to take into account the ca
che system. There is a well known abstract interpretation for LRU caches\,
based on "ages"\; no such analyses are known for other cache policies. In
deed\, the common wisdom is that "pseudo LRU" caches are hard to analyse b
ecause their behavior may depend on events in the distant past that one ca
nnot be sure to have flushed away.\n\nIn this talk:\n- We show how this co
mmon wisdom can be grounded in strong theory: we prove that\, in a certain
model\, exact static analysis for two kinds of pseudo LRU caches and for
FIFO is PSPACE-complete\, while that for LRU is "only" NP-complete.\n- We
give a practical algorithm for exact static analysis for LRU. This analysi
s has been implemented in the OTAWA tool.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Verifying Concurrent Randomized Programs - Joseph Tassarotti\, Bos
ton College
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200110T100000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200110T110000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1046
DESCRIPTION:Despite continued progress in program verification\, many fund
amental data structures and algorithms remain difficult to verify. Challen
ges arise when programs use concurrency or randomization because these eff
ects lead to non-deterministic behavior. Although many specialized logics
have been developed to reason about programs that use either concurrency o
r randomization\, most can only handle the use of one of these features in
isolation. However\, many common concurrent data structures are randomize
d\, making it important to consider the combination.\n\nThis talk will des
cribe Polaris\, a logic for reasoning about programs that are both concurr
ent and randomized. Polaris combines ideas from three separate lines of wo
rk: (1) Varacca and Winskel's denotational model of non-determinism and pr
obability\, (2) Barthe et al.'s approach to probabilistic relational reaso
ning via couplings\, and (3) higher-order concurrent separation logic\, as
realized in the Iris verification framework.
LOCATION:Salle 3052
END:VEVENT
BEGIN:VEVENT
SUMMARY:Nash equilibria in games on graphs equipped with a communication m
echanism - Nathan Thomasset\, LSV & ENS de Scalay
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200309T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200309T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1048
DESCRIPTION:We study infinite games played on graphs\, in which players mo
ve a token along the edges of a graph. Each player has certain preferences
over the resulting infinite path taken by the token\, and will choose the
ir actions accordingly. In this setting\, we are particularly interesting
in Nash equilibria\, which describe a course of action such that no player
has any incentive to deviate and is thus seen as a rational outcome of th
e game. We add a communication mechanism to the classical setting\, such t
hat players can send information to and receive information from other pla
yers\, and we show that the resulting Nash equilibria can be expressed wit
h a very simple communication scheme\, thus allowing us to design an algor
ithm to compute them.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Towards a Proof Theory of Probabilistic Logics - [Cancelled] Matte
o Mio\, CNRS & ENS de Lyon
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200316T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200316T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1057
DESCRIPTION:Probabilistic Logics are formal languages designed to express
properties of probabilistic programs. For most probabilistic logics severa
l key problems are still open. One of such problems is to design convenien
t analytical proof systems in the style of Gentzen sequent calculus. This
is practically important in order to simplify the task of proof search: th
e CUT-elimination theorem greatly reduces the search space. In this talk I
will present some recent developments in this direction.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Deriving Parsers\, Deriving Type Systems - Viktor Kuncak\, EPFL
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200511T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200511T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1058
DESCRIPTION:I will present two recent results from my research group.\nFir
st\, I will show the notion of Brzozowski derivative of a formal language
can be combined with the zipper data structure and used to construct effic
ient LL(1) parsers [1] (joint work with Romain Edelmann and Jad Hamza).\nS
econd\, I will present System FR\, an expressive dependent type system wit
h refinement types and subtyping\, whose design is guided by interpretatio
n of types as sets of terms [2] (joint work with Jad Hamza and Nicolas Voi
rol)\, and which serves as foundation of Stainless verifier for Scala [3].
\n\n[1] http://lara.epfl.ch/~kuncak/paper/EdelmannETAL20ZippyLLParsingDeri
vatives.pdf\n[2] http://lara.epfl.ch/~kuncak/papers/HamzaETAL19SystemFR.pd
f\n[3] https://stainless.epfl.ch/
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Real-time systems compilation - Dumitru Potop-Butucaru\, INRIA Par
is
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200504T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200504T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1059
DESCRIPTION:I introduce and advocate for the concept of Real-Time Systems
Compilation. By analogy with classical compilation\, real-time systems co
mpilation consists in the fully automatic construction of running\, correc
t-by-construction implementations from functional and non-functional speci
fications of embedded control systems. Like in a classical compiler\, the
whole process must be fast (thus enabling a trial-and-error design style)
and produce reasonably efficient code. This requires the use of fast heuri
stics\, and the use of fine-grain platform and application models. Unlike
a classical compiler\, a real-time systems compiler must take into account
non-functional properties of a system and ensure the respect of non-funct
ional requirements (in addition to functional correctness). I also present
Lopht\, a real-time systems compiler we built by combining techniques and
concepts from real-time scheduling\, compilation\, and synchronous langua
ges.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Lower bounds for polynomial recurrence sequences - [Rescheduled] F
ilip Mazowiecki\, MPI SWS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200330T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200330T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1063
DESCRIPTION:We study the expressiveness of polynomial recurrence sequences
(PRS)\, a nonlinear extension of the well-known class of linear recurrenc
e sequences (LRS). A typical example of a sequence definable in PRS but no
t in LRS is a_n = n!. Our main result is that the sequence u_n = n^n canno
t be defined by any PRS. We also discuss the impact of our results on the
expressiveness of nonlinear extensions of weighted automata.\nThis is join
t work with Michaël Cadilhac\, Charles Paperman\, Michał Pilipczuk and G
éraud Sénizergues.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Semantics for Persistent Memory - Viktor Vafeiadis\, MPI
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200518T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200518T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1064
DESCRIPTION:Non-volatile memory (NVM) is emerging as a technology that may
significantly impact the computing landscape in the near future. NVM ensu
res durability of data across power failures (i.e.\, as hard drives do) at
a performance close to that of conventional volatile memory (RAM). Nevert
heless\, NVM is quite difficult to use correctly because of data caches: t
he writes do not persist to memory immediately when performed by a program
and may further be reordered. In order to ensure that writes are propagat
ed to memory in the correct order and that all writes have persisted to me
mory\, the programmers have to use special barrier and cache flushing inst
ructions.\n\nThe talk will discuss the semantics of such instructions\, ho
w they interact with the architecture's weak consistency model\, and how t
hey can be used to develop higher-level primitives for safe persistent pro
gramming.
LOCATION:(online using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Reachability problem for fixed dimensional VASSes - [Rescheduled]
Wojciech Czerwinski\, University of Warsaw
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200427T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200427T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1067
DESCRIPTION:I will present a few recent results about reachability problem
for fixed dimensional VASSes. There results invalidate some previously po
sed conjectures and show that the problem is harder than previously expect
ed to be.\n\nThis is a joint work with Sławomir Lasota\, Ranko Lazic\, Je
rome Leroux and Filip Mazowiecki.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Games with arbitrarily many players - Nathalie Bertrand\, INRIA Re
nnes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200629T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200629T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1081
DESCRIPTION:Traditional concurrent games on graphs involve a fixed number
of players\, who\ntake decisions simultaneously\, determining the next sta
te of the game. With\nAnirban Majumdar and Patricia Bouyer\, we introduced
a parameterized variant of\nconcurrent games on graphs\, where the parame
ter is precisely the number of\nplayers. Parameterized concurrent games ar
e described by finite graphs\, in which\nthe transitions bear finite-word
languages to describe the possible move\ncombinations that lead from one v
ertex to another.\n\nWe report on results on two problems for so-called pa
rameterized concurrent\ngames. To start with\, we tackled the problem of d
etermining whether the first\nplayer\, say Eve\, has a strategy to ensure
a reachability objective against any\nstrategy profile of her opponents a
s a coalition. In particular Eve's strategy\nshould be independent of the
number of opponents she actually has. We establish\nthe precise complexiti
es of the parameterized reachability game problem. Second\,\nwe consider a
synthesis problem\, where one aims at designing a strategy for each\nof t
he players so as to achieve a common objective. For safety objectives\, we
\nshow that this kind of distributed synthesis problem is decidable.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:An Operational Guide to Monitorability - [Cancelled] Adrian Franca
lanza\, University of Malta
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200330T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200330T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1097
DESCRIPTION:Monitorability underpins the technique of Runtime Verification
because it delineates what properties can be verified at runtime. Althoug
h many monitorability definitions exist\, few are defined explicitly in te
rms of the operational guarantees provided by monitors\, that is the compu
tational entities carrying out the verification. We view monitorability as
a spectrum\, where the fewer guarantees that are required of monitors\, t
he more properties become monitorable. Accordingly\, we present a monitora
bility hierarchy based on this trade-off. For regular specifications\, we
give syntactic characterizations in terms of Hennessy–Milner logic with
recursion for its levels. Finally\, we map existing monitorability definit
ions into our hierarchy. Hence our work gives a unified framework that mak
es the operational assumptions and guarantees of each definition explicit.
This provides a rigorous foundation that can inform design choices and co
rrectness claims for runtime verification tools.
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:Polynomial Invariants for Affine Programs and Introduction to Alge
braic Geometry (for computer scientists) - Amaury Pouly\, CNRS & IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200406T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200406T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1113
DESCRIPTION:In this talk I will present some results we obtained in LICS 2
018\nwhere we exhibit an algorithm to compute the strongest polynomial (or
\nalgebraic) invariants that hold at each location of a given affine\nprog
ram (i.e.\, a program having only non-deterministic (as opposed\nto condit
ional) branching and all of whose assignments are given\nby affine express
ions). Our main tool is an algebraic result of inde-\npendent interest: gi
ven a finite set of rational square matrices of\nthe same dimension\, we s
how how to compute the Zariski closure\nof the semigroup that they generat
e.\n\nI will then give a small introduction to algebraic geometry for\ncom
puter scientisits. The goal it to give the background necessary\nto unders
tand how the proof works: we will talk about algebraic\nsets/varieties and
constructible/definable sets.\n\nIn a second talk on April 20th\, I will
give use the material introduced\nin this talk to explain the algorithm fo
r computing the Zariski closure\nof a group and semigroup of matrices.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Polynomial Invariants for Affine Programs and Introduction to Alge
braic Geometry (for computer scientists) - Amaury Pouly\, CNRS & IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200420T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200420T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1114
DESCRIPTION:In this talk I will present some results we obtained in LICS 2
018 where we exhibit an algorithm to compute the strongest polynomial (or
algebraic) invariants that hold at each location of a given affine program
(i.e.\, a program having only non-deterministic (as opposed to conditiona
l) branching and all of whose assignments are given by affine expressions)
. Our main tool is an algebraic result of inde- pendent interest: given a
finite set of rational square matrices of the same dimension\, we show how
to compute the Zariski closure of the semigroup that they generate.\n\nI
will then give a small introduction to algebraic geometry for computer sci
entisits. The goal it to give the background necessary to understand how t
he proof works: we will talk about algebraic sets/varieties and constructi
ble/definable sets.\n\nIn a second talk on April 20th\, I will give use th
e material introduced in this talk to explain the algorithm for computing
the Zariski closure of a group and semigroup of matrices.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:SMT-Friendly Formalization of the Solidity Memory Model - Akos Haj
du\, Budapest University of Technology and Economics
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200415T150000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200415T160000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1115
DESCRIPTION:Solidity is the dominant programming language for smart contra
cts on the Ethereum blockchain. This talk presents a high-level formalizat
ion of the Solidity language with a focus on the memory model. The memory
model of Solidity has various unusual and non-trivial behaviors\, providin
g a fertile ground for potential bugs. Smart contracts have access to two
classes of data storage: a permanent storage that is a part of the global
blockchain state\, and a transient local memory used when executing transa
ctions. While the local memory uses a standard heap of entities with refer
ences\, the permanent storage has pure value semantics (although pointers
to storage can be declared locally). This memory model that combines both
value and reference semantics - with all interactions between the two - po
ses some interesting challenges but also offers great opportunities for au
tomation. The presented formalization covers all features of the language
related to managing state and memory in an effective way: all but few feat
ures can be encoded in the quantifier-free fragment of standard SMT theori
es. This enables precise and efficient reasoning about the state of smart
contracts written in Solidity. The formalization is implemented in the sol
c-verify tool and we provide an evaluation on an extensive test set that v
alidates the semantics and shows the novelty of the approach compared to o
ther Solidity-level contract analysis tools.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Deterministic membership and separability problems for timed autom
ata - Lorenzo Clemente\, Warsaw university
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200622T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200622T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1135
DESCRIPTION:In this talk we survey the deterministic membership and determ
inistic separability problems for timed automata. In the deterministic mem
bership problem (a.k.a. determinisability) we are given in input a nondete
rministic timed automaton (NTA) and we have to decide whether there is a d
eterministic timed automaton (DTA) recognising the same language. In the d
eterministic separability problem\, we are given in input two NTA and we h
ave to decide whether there is a DTA separating them.\n\nWe survey decidab
ility and undecidability results for these two problems\nand for their var
iants where we put restrictions on the number of clocks of the input NTA a
nd/or the output DTA. While the deterministic separability problem has bee
n studied before in the timed automata literature (mostly with undecidabil
ity results)\, the separability problem does not appear to have been addre
ssed before.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:On the structure of solution sets to regular word equations. - Joe
l Day\, Loughborough University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200608T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200608T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1136
DESCRIPTION:For quadratic word equations\, there exists an algorithm based
on rewriting rules which generates a directed graph describing all soluti
ons to the equation. For regular word equations – those for which each v
ariable occurs at most once on each side of the equation – we investigat
e the properties of this graph\, such as bounds on its diameter\, size\, a
nd DAG-width\, as well as providing some insights into symmetries in its s
tructure. As a consequence\, we obtain a combinatorial proof that the prob
lem of deciding whether a regular word equation has a solution is in NP.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Local Reasoning About the Presence of Bugs: Incorrectness Separati
on Logic - Azalea Raad\, Imperial College London
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200615T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200615T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1137
DESCRIPTION:There has been a great deal of work on local reasoning about s
tate for proving the absence of bugs\, but none for proving the presence o
f bugs. In this paper\, we present a new formal framework for local reason
ing about the presence of bugs\, building on two complementary foundations
: (1) separation logic and (2) the recently introduced "incorrectness logi
c". In addition to exploring the theory of this new incorrectness separati
on logic (ISL)\, we show how it can be used to derive a begin-anywhere\, i
ntra-procedural forward symbolic execution analysis that has no false posi
tives by construction. In so doing\, we take a step towards transferring m
odular\, scalable techniques from the world of program verification to the
world of bug catching.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Approximating Values of Generalized-Reachability Stochastic Games
- Jan Kretinsky\, Technical University of Munich
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200713T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200713T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1143
DESCRIPTION:Simple stochastic games are turn-based 2.5-player games with a
reachability objective. The basic question asks whether one player can en
sure reaching a given target with at least a given probability. A natural
extension is games with a conjunction of such conditions as objective. Des
pite a plethora of recent results on the analysis of systems with multiple
objectives\, the decidability of this basic problem remains open. In this
paper\, we present an algorithm approximating the Pareto frontier of the
achievable values to a given precision. Moreover\, it is an anytime algori
thm\, meaning it can be stopped at any time returning the current approxim
ation and its error bound.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:O-minimal invariants for discrete and continuous linear dynamical
systems - Shaull Almagor\, Technion Computer Science Faculty
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200525T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200525T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1146
DESCRIPTION:Linear dynamical systems are used extensively in mathematics\,
computer science\, physics\, and engineering\, to model the evolution of
a system over (discrete or continuous) time. Rechability analysis of such
systems thus plays a key role in many areas of computer science\, includin
g program verification\, abstract\ninterpretation\, robotic motion plannin
g\, and many more. Already for the simplest variants of linear dynamical s
ystems\, the question of termination relates to deep open problems in numb
er theory\, such as the decidability of the Skolem and Positivity Problems
.\n\nIn this talk\, we introduce the class of o-minimal invariants\, which
is\nbroader than any previously considered\, and study the decidability o
f\nthe existence and algorithmic synthesis of such invariants as\ncertific
ates of non-reachability for dynamical systems\, equipped with a large\ncl
ass of halting conditions. In the discrete setting\, we establish two main
decidability results\, one of them conditional on Schanuel's conjecture i
n transcendental number theory. We then examine the continuous setting\, a
nd the challenges that arise there. We establish some decidability resutls
\, and some conditional decidability results. We also demonstrate the hard
ness of a remaining case\, with respect to open problems in number theory.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Perfectly Parallel Fairness Certification of Neural Networks - Cat
erina Urban\, INRIA- ENS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200603T140000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200603T150000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1155
DESCRIPTION:Recently\, there is growing concern that machine-learning mode
ls\, which currently assist or even automate decision making\, reproduce\,
and in the worst case reinforce\, bias of the training data. The developm
ent of tools and techniques for certifying fairness of these models or des
cribing their biased behavior is\, therefore\, critical. In this paper\, w
e propose a perfectly parallel static analysis for certifying causal fairn
ess of feed-forward neural networks used for classification of tabular dat
a. When certification succeeds\, our approach provides definite guarantees
\, otherwise\, it describes and quantifies the biased behavior. We design
the analysis to be sound\, in practice also exact\, and configurable in te
rms of scalability and precision\, thereby enabling pay-as-you-go certific
ation. We implement our approach in an open-source tool and demonstrate it
s effectiveness on models trained with popular datasets.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:Strategy Complexity: Finite Systems vs. Infinite Systems - Richard
Mayr\, University of Edinburgh
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200706T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200706T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1156
DESCRIPTION:Consider 2-player perfect information turn-based stochastic ga
mes on finite or infinite graphs\, and sub-cases (e.g.\, Markov decision p
rocesses (MDPs)). Depending on the objective of the game\, optimal strateg
ies (where they exist) and epsilon-optimal strategies may need to use a ce
rtain amount/type of memory or to use randomization. This is called the st
rategy complexity of the objective on the given class of games. We give an
overview over the strategy complexity of common objectives on games and M
DPs\, with a particular focus on the differences between finite-state game
s/MDPs and infinite-state games/MDPs.
LOCATION:(online\, using BigBlueButton)
END:VEVENT
BEGIN:VEVENT
SUMMARY:A Hennessy-Milner Theorem for ATL with Imperfect Information - Cat
alin Dima\, LACL\, Université Paris-Est Créteil
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20201019T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20201019T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1186
DESCRIPTION:We show that a history-based variant of alternating bisimulati
on with imperfect information allows it to be related to a variant of Alte
rnating-time Temporal Logic (ATL) with imperfect information by a full Hen
nessy-Milner theorem. The variant of ATL we consider has a common knowledg
e semantics\, which requires that the uniform strategy available for a coa
lition to accomplish some goal must be common knowledge inside the coaliti
on\, while other semantic variants of ATL with imperfect information do no
t accomodate a Hennessy-Milner theorem. We also show that the existence of
a history-based alternating bisimulation between two finite Concurrent Ga
me Structures with imperfect information (iCGS) is undecidable.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Monte Carlo Tree Search guided by Symbolic Advice for MDPs - Damie
n Busatto\, Université Libre de Bruxelles
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20201102T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20201102T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1207
DESCRIPTION:We consider the online computation of a strategy that aims at
optimizing the expected average reward in a Markov decision process. The s
trategy is computed with a receding horizon and using Monte Carlo tree sea
rch (MCTS). We augment the MCTS algorithm with the notion of symbolic advi
ce\, and show that its classical theoretical guarantees are maintained. Sy
mbolic advice are used to bias the selection and simulation strategies of
MCTS. We describe how to use QBF and SAT solvers to implement symbolic adv
ice in an efficient way. We illustrate our new algorithm using the popular
game Pac-Man and show that the performances of our algorithm exceed those
of plain MCTS as well as the performances of human players.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Formal verification of stochastic systems using Markov chains and
dynamic Bayesian networks - Sadegh Soudjani\, School of Computing\, Newcas
tle University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20201109T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20201109T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1232
DESCRIPTION:In this talk I address the problem of finite-horizon probabili
stic safety for discrete-time stochastic systems over general (uncountable
or hybrid) state spaces. I show how to compute discrete-time\, finite sta
te Markov chains as formal abstractions of such systems. The abstraction d
iffers from existing approaches in two ways. First\, it exploits the struc
ture of the underlying system to compute the abstraction separately for ea
ch dimension. Second\, it employs dynamic Bayesian networks (DBN) as compa
ct representations of the abstraction. In contrast\, existing approaches r
epresent and store the (exponentially large) Markov chain explicitly\, whi
ch leads to heavy memory requirements.\nI show how to construct a DBN abst
raction of a Markov process satisfying an independence assumption on the d
riving process noise. Guaranteed bounds on the error in the abstraction ca
n be computed with respect to the probabilistic safety property. Additiona
lly\, I show how factor graphs and the sum-product algorithm for DBNs can
be used to solve the finite-horizon probabilistic safety problem. Together
\, DBN-based representations and algorithms can be significantly more effi
cient than explicit representations of Markov chains for abstracting and m
odel checking structured Markov processes. I will also briefly discuss two
of the tools for Markov chain abstraction: FAUST2 and Amytiss.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Deciding ω-Regular Properties on Linear Recurrence Sequences - Ed
on Kelmendi\, University of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20201123T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20201123T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1233
DESCRIPTION:We consider the problem of deciding ω-regular properties on i
nfinite traces produced by linear loops. Here we think of a given loop as
producing a single infinite trace that encodes information about the signs
of program variables at each time step. Formally\, our main result is a p
rocedure that inputs a prefix-independent ω-regular property and a sequen
ce of numbers satisfying a linear recurrence\, and determines whether the
sign description of the sequence (obtained by replacing each positive entr
y with "+"\, each negative entry with "−"\, and each zero entry with "0"
) satisfies the given property. Our procedure requires that the recurrence
be simple\, \\ie\, that the update matrix of the underlying loop be diago
nalisable. This assumption is instrumental in proving our key technical le
mma: namely that the sign description of a simple linear recurrence sequen
ce is almost periodic in the sense of Muchnik\, Semënov\, and Ushakov. To
complement this lemma\, we give an example of a linear recurrence sequenc
e whose sign description fails to be almost periodic. Generalising from si
gn descriptions\, we also consider the verification of properties involvin
g semi-algebraic predicates on program variables. This is joint work with:
Shaull Almagor\, Toghrul Karimov\, Jöel Ouaknine\, and James Worrell.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Structural Invariants for the Verification of Systems with (Recurs
ively Defined) Parameterized Architectures - Radu Iosif\, Verimag\, CNRS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20201116T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20201116T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1234
DESCRIPTION:We consider parameterized concurrent systems consisting of a f
inite but unknown number of components\, obtained by replicating a given s
et of finite state automata. Components communicate by executing atomic in
teractions whose participants update their states simultaneously. We intro
duce an interaction logic to specify both the type of interactions (e.g. r
endez-vous\, broadcast) and the topology of the system (e.g. pipeline\, ri
ng). Proving safety properties of such a parameterized system\, like deadl
ock freedom or mutual exclusion\, requires inferring an inductive invarian
t that contains all reachable states of all system instances and no unsafe
state. We present a method to automatically synthesize inductive invarian
ts directly from the formula describing the interactions\, without costly
fixed point iterations. The invariants are defined using the WSkS fragment
of the monadic second order logic\, known to be decidable by a classical
automata-logic connection. This reduces the safety verification problem to
checking satisfiability of a WSkS formula. We experimentally prove that t
his invariant is strong enough to verify safety properties of a large numb
er of systems including textbook examples (dining philosophers\, synchroni
zation schemes)\, classical mutual exclusion algorithms\, cache-coherence
protocols and self-stabilization algorithms\, for an arbitrary number of c
omponents. \n\nIf time allows\, in the second part of this talk I wil
l describe a term algebra as a new formal specification language for the c
oordinating architectures of distributed systems consisting of a finite ye
t unbounded number of components. The language allows to describe infinite
sets of systems whose coordination between components share the same patt
ern\, using inductive definitions similar to the ones used to describe alg
ebraic data types or recursive data structures. Further\, we give a verifi
cation method for the parametric systems described in this language\, rely
ing on the automatic synthesis of structural invariants that enable provin
g general safety properties (mutual exclusion\, absence of deadlocks).
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:On Information Control in Probabilistic Systems: a closer look on
Opacity and Diagnosis - Engel Lefaucheux\, Max-Planck Institute for Softwa
re Systems\, Sarrebrucken
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20201130T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20201130T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1245
DESCRIPTION:The control of the information given by a system has recently
seen increasing importance due to the omnipresence of communicating system
s\, the need for privacy\, etc.\nThis control can be used in order to disc
lose to an observer an information of the system\, or\, oppositely\, to hi
de one.\nIn this talk\, I will consider the control of the information rel
eased by a system represented by a stochastic model such as a Markov chain
.\nHere\, an external observer is interested in detecting a particular set
of relevant paths of the system.\nHowever\, he can only observe those pat
hs through an observation function which obfuscates the real behaviour of
the system.\nExact disclosure of the information occurs when the observer
can deduce from a finite observation that the path is relevant\, the appro
ximate disclosure variant corresponding to the path being identified as re
levant with high accuracy.\nI will discuss the problems of diagnosability
and opacity\, which corresponds\, in spirit\, to the cases where one wants
to disclose all the information or hide as much of it as possible with a
focus on the approximate notion of disclosure.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Logics and automata over infinite message sequence charts - Marie
Fortin\, University of Liverpool
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20201207T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20201207T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1261
DESCRIPTION:Communicating finite-state machines (CFMs) are a standard mode
l of concurrent message-passing systems. They consist of a fixed number of
finite-state processes communicating through unbounded point-to-point FIF
O channels\, and they define languages of partial orders called message se
quence charts (MSCs)\, representing possible executions of the system. In
this talk\, I will review past and recent characterizations of the express
ive power of CFMs\, in the spirit of Büchi-Elgot-Trakhtenbrot theorem for
finite automata. Our main result is that\, both for finite and infinite e
xecutions\, CFMs have the same expressive power as existential monadic sec
ond-order logic (EMSO). As a corollary\, we obtain a new proof of a known
characterization in the restricted case where the channels are assumed to
be of bounded size\, namely\, that CFMs are equivalent to full MSO logic o
ver finite existentially-bounded MSCs. We also extend that result from fin
ite to infinite executions. For the main result\, where channels are assum
ed to be unbounded\, the proof relies on another logic of independent inte
rest: a star-free variant of propositional dynamic logic based on operatio
ns similar to LTL "since" and "until" modalities. This logic is equivalent
to first-order logic\, and its formulas can be translated into equivalent
CFMs of exponential size (on the other hand\, the translation from first-
order logic is non-elementary). This is joint work with Benedikt Bollig an
d Paul Gastin.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Analysing installation scenarios of Debian packages - Nicolas Jean
nerod\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20201214T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20201214T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1266
DESCRIPTION:Debian GNU/Linux is a Linux distribution composed of free and\
nopen-source software. It is heavily used all over the world as an\noperat
ing system for personal computers and servers\, and is the basis\nfor many
other distributions.\n\nDeban currently includes more than 28 thousand ma
intainer scripts\,\nalmost all of them written in POSIX shell. These scrip
ts are executed\nwith root privileges at installation\, update\, and remov
al of a\npackage\, which make them critical for system maintenance. While
Debian\npolicy provides guidance for package maintainers producing the\nsc
ripts\, few tools exist to check the compliance of a script to it.\n\nThis
presentation reports on the application of a formal verification\napproac
h based on symbolic execution to find violations of some\nnon-trivial prop
erties required by Debian policy in maintainer\nscripts. We present our me
thodology and give an overview of the\ntoolchain. We focus in particular o
n the tree logics used to represent\nsymbolically a file system transforma
tion\, and the use of such a logic\nin the symbolic engine.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Parameterized verification under TSO is PSPACE-complete. - Mohamed
Faouzi Atig\, Uppsala University
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210111T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210111T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1279
DESCRIPTION:We consider parameterized verification of concurrent programs
under the Total Store Order (TSO) semantics. A program consists of a set o
f processes that share a set of variables on which they can perform read a
nd write operations. We show that the reachability problem for a system co
nsisting of an arbitrary number of identical processes is PSPACE-complete.
We prove that the complexity is reduced to polynomial time if the process
es are not allowed to read the initial values of the variables in the memo
ry. When the processes are allowed to perform atomic read-modify-write ope
rations\, the reachability problem has a non-primitive recursive complexit
y.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Global PAC Bounds for Learning Discrete Time Markov Chains. - Blai
se Genest\, IRISA (CNRS)
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210208T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210208T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1280
DESCRIPTION:Learning models from observations of a system is a powerful to
ol with many applications. In this paper\, we consider learning Discrete T
ime Markov Chains (DTMC)\, with different methods such as frequency estima
tion or Laplace smoothing. While models learnt with such methods converge
asymptotically towards the exact system\, a more practical question in the
realm of trusted machine learning is how accurate a model learnt with a l
imited time budget is. Existing approaches provide bounds on how close the
model is to the original system\, in terms of bounds on local (transition
) probabilities\, which has unclear implication on the global behavior.\n\
nIn this work\, we provide global bounds on the error made by such a learn
ing process\, in terms of global behaviors formalized using temporal logic
. More precisely\, we propose a learning process ensuring a bound on the e
rror in the probabilities of these properties. While such learning process
cannot exist for the full LTL logic\, we provide one ensuring a bound tha
t is uniform over all the formulas of CTL. Further\, given one time-to-fai
lure property\, we provide an improved learning algorithm. Interestingly\,
frequency estimation is sufficient for the latter\, while Laplace smoothi
ng is needed to ensure non-trivial uniform bounds for the full CTL logic.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Succinct Population Protocols for Presburger Arithmetic - Martin H
elfrich\, Technical University of Munich
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210215T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210215T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1281
DESCRIPTION:In [Dana Angluin et al.\, 2006]\, Angluin et al. proved that p
opulation protocols compute exactly the predicates definable in Presburger
arithmetic (PA)\, the first-order theory of addition. As part of this res
ult\, they presented a procedure that translates any formula φ of quantif
ier-free PA with remainder predicates (which has the same expressive power
as full PA) into a population protocol with 2^????(poly(|φ|)) states tha
t computes φ. More precisely\, the number of states of the protocol is ex
ponential in both the bit length of the largest coefficient in the formula
\, and the number of nodes of its syntax tree. In this paper\, we prove th
at every formula φ of quantifier-free PA with remainder predicates is com
putable by a leaderless population protocol with ????(poly(|φ|)) states.
Our proof is based on several new constructions\, which may be of independ
ent interest. Given a formula φ of quantifier-free PA with remainder pred
icates\, a first construction produces a succinct protocol (with ????(|φ|
³) leaders) that computes φ\; this completes the work initiated in [Mich
ael Blondin et al.\, 2018]\, where we constructed such protocols for a fra
gment of PA. For large enough inputs\, we can get rid of these leaders. If
the input is not large enough\, then it is small\, and we design another
construction producing a succinct protocol with one leader that computes
φ. Our last construction gets rid of this leader for small inputs.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Active learning of timed automata with unobservable resets - Léo
Henry\, IRISA\, Université de Rennes I
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210118T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210118T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1282
DESCRIPTION:Active learning of timed languages is concerned with the infer
ence of timed automata from observed timed words. The agent can query for
the membership of words in the target language\, or propose a candidate mo
del and verify its equivalence to the target. The major difficulty of this
framework is the inference of clock resets\, central to the dynamics of t
imed automata\, but not directly observable. Interesting first steps have
already been made by restricting to the subclass of event-recording automa
ta\, where clock resets are tied to observations. In order to advance towa
rds learning of general timed automata\, we generalize this method to a ne
w class\, called reset-free event-recording automata\, where some transiti
ons may reset no clocks. This offers the same challenges as generic timed
automata while keeping the simpler framework of event-recording automata f
or the sake of readability. Central to our contribution is the notion of i
nvalidity\, and the algorithm and data structures to deal with it\, allowi
ng on-the-fly detection and pruning of reset hypotheses that contradict ob
servations\, a key to any efficient active-learning procedure for generic
timed automata.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Connected multi-agent path finding - François Schwarzentruber\, I
RISA\, ENS Rennes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210201T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210201T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1290
DESCRIPTION:Motivated by the increasing appeal of robots in information-ga
thering missions\, we study multi-agent path planning problems in which th
e agents must remain interconnected. We model an area by a topological gra
ph specifying the movement and the connectivity constraints of the agents.
In the first part of the talk\, we study the theoretical complexity of th
e reachability and the coverage problems of a fleet of connected agents. W
e also introduce a new class called sight-moveable graphs which admit effi
cient algorithms. In the second part\, we re-visit the conflict-based sear
ch algorithm known for multi-agent path finding\, and define a variant whe
re conflicts arise from disconnections rather than collisions.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:On the formal verification of safety-critical systems: challenges\
, approaches and perspectives - Mohammed Foughali\, Vérimag\, Université
Grenoble-Alpes
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210222T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210222T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1301
DESCRIPTION:Safety-critical applications\, e.g. those stemming from roboti
c\, autonomous and cyber-physical systems\, must be formally verified agai
nst crucial behavioral and timed properties. Yet\, the use of formal verif
ication techniques in such context faces a number of challenges\, such as
the absence of formal foundations of robotic frameworks and the lack of sc
alability of exhaustive verification techniques. In this talk\, I will exp
lore the approaches I have been proposing for the last six years to tackle
these challenges\, based on a global vision that favors correctness\, use
r-friendliness and scalability of formal methods vis-à-vis real-world rob
otic and autonomous systems deployed on embedded platforms. I will discuss
a major part of my work where safety-critical specifications are automati
cally translated into strictly equivalent formal models on which model che
cking\, but also scalable non exhaustive techniques such as statistical mo
del checking and runtime verification\, may be used by practitioners to ga
in a considerable amount of trust in their underlying applications. Furthe
r\, I will present a couple of techniques that allow to take into account
hardware and OS specificities in the verification process\, such as the sc
heduling policy and the number of processor cores provided by the platform
\, and thus increase the meaningfulness of the verification results. I wil
l conclude with possible future research directions within the broad objec
tive of deploying trustable safety-critical systems through bridging the g
ap between the software engineering\, robotics\, formal methods and real-t
ime systems communities.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Reifying Concurrent Programs - Shaz Qadeer\, Novi Research\, Seatt
le
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210225T160000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210225T170000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1315
DESCRIPTION:Program reification is a new approach to the construction of v
erified\nconcurrent programs and their proofs. This approach simplifies a
nd scales\n(human and automated) reasoning by enabling a concurrent progra
m to be\nrepresented and manipulated at multiple layers of abstraction. T
hese\nabstraction layers are chained together via simple program transform
ations\;\neach transformation is justified by a collection of automaticall
y checked\nverification conditions. Program reification makes proofs maint
ainable and\nreusable\, specifically eliminating the need to write complex
invariants on\nthe low-level encoding of the concurrent program as a flat
transition\nsystem.\n\nI will present Civl\, a reifier for concurrent pro
grams. Civl has been used\nto construct verified low-level implementation
s of complex systems such as a\n concurrent garbage collector\, consensus
protocol\, and shared-memory data\nstructures. Civl is publicly available
: https://civl-verifier.github.io/\n.\n\nThis work has been done jointly with Bern
hard Kragl (IST Austria).
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Cyclotomic Identity Testing and Applications - Mahsa Shirmohammadi
\, IRIF\, CNRS
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210301T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210301T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1316
DESCRIPTION:We consider the cyclotomic identity testing (CIT) problem: giv
en a polynomial~$f(x_1\,\\ldots\,x_k)$\, decide whether $f(\\zeta_n^{e_1}\
,\\ldots\,\\zeta_n^{e_k})$ is zero\, where $\\zeta_n = e^{2\\pi i/n}$ is a
primitive complex $n$-th root of unity and $e_1\,\\ldots\,e_k$ are intege
rs\, represented in binary. When~$f$ is given by an algebraic circuit\, we
give a randomized polynomial-time algorithm for CIT assuming the general
ised Riemann hypothesis (GRH)\, and show that the problem is in coNP un
conditionally. When $f$ is given by a circuit of polynomially bounded degr
ee\, we give a randomized NC algorithm. In case $f$ is a linear form we sh
ow that the problem lies in NC. Towards understanding when CIT can be solv
ed in deterministic polynomial-time\, we consider so-called diagonal depth
-3 circuits\, i.e.\, polynomials $f=\\sum_{i=1}^m g_i^{d_i}$\, where $g_i$
is a linear form and $d_i$ a positive integer given in unary. We observe
that a polynomial-time algorithm for CIT on this class would yield a sub-
exponential-time algorithm for polynomial identity testing. However\, ass
uming GRH\, we show that if the linear forms~$g_i$ are all identical then
CIT can be solved in polynomial time. Finally\, we use our results to give
a new proof that equality of compressed strings\, i.e.\, strings presente
d using context-free grammars\, can be decided in randomized NC.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:How to play in infinite MDPs - Stefan Kiefer\, University of Oxfor
d
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210315T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210315T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1345
DESCRIPTION:Markov decision processes (MDPs) are a standard model for dyna
mic systems that exhibit both stochastic and nondeterministic behavior. Fo
r MDPs with finite state space it is known that for a wide range of object
ives there exist optimal strategies that are memoryless and deterministic.
In contrast\, if the state space is infinite\, the picture is much richer
: optimal strategies may not exist\, and optimal or epsilon-optimal strate
gies may require (possibly infinite) memory. Based on many examples\, I am
going to give an introduction to a collection of techniques that allow fo
r the construction of strategies with little or no memory in countably inf
inite MDPs.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Dynamical Systems and Program Analysis - James Worrell\, Universit
y of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210322T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210322T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1346
DESCRIPTION:This talk is about the algorithmic analysis of dynamical syste
ms and its relevance to the foundations of program analysis. A dynamical s
ystem is a state-based system that is specified by a rule specifying how t
he state changes over time (e.g.\, a swinging pendulum or a cobweb model o
f supply and demand in economics). While the study of dynamical systems pe
rmeates the quantitative sciences\, in this talk we focus on computational
aspects and their relevance to basic verification problems\, such as term
ination and invariant synthesis. We highlight in particular certain proble
ms that can be traced back to the program-analysis literature\, e.g.\, con
cerning the decidability of termination for linear constraint loops and th
e computability of polyhedral and polynomial invariants for various classe
s of transition systems. In the talk we give some of the mathematical cont
ext of these problems\, discuss recent progress\, and highlight unsolved c
ases. The characteristic feature of the problems we consider is that they
turn out to be much more challenging than they might first appear to the i
nnocent-minded and in some cases have connections to problems at the front
iers of modern mathematics.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Flat Petri nets - Jérôme Leroux\, LABRI
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210412T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210412T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1347
DESCRIPTION:Vector addition systems with states (VASS)\, or equivalently v
ector addition systems\, or Petri nets are a long established model of con
currency with extensive applications. The central algorithmic problem is r
eachability: whether from a given initial configuration there exists a seq
uence of valid execution steps that reaches a given final configuration. T
he complexity of the problem has remained unsettled since the 1960s\, and
it is one of the most prominent open questions in the theory of computatio
n.\n\nIn this presentation\, we survey results about the reachability prob
lem focusing on flat VASS. This subclass is central for computing the reac
hability set of general VASS using Presburger arithmetic. In fact\, the re
achability set of a VASS is Presburger if\, and only if\, it is flattable\
, i.e. the computation of its reachability set is reducible to the computa
tion of the reachability set of a flat VASS. Whereas the reachability prob
lem for flat VASS is clearly NP-complete in any fix dimension when numbers
are encoded in binary\, finding the exact complexity of the reachability
problem for flat VASS in unary is a difficult (still open) problem.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Observation and Distinction. Representing Information in Infinite
Games - Laurent Doyen\, LMF — ENS Saclay
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210510T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210510T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1388
DESCRIPTION:We compare two approaches for modelling imperfect information
in\ninfinite games by using finite-state automata. The first\, more standa
rd\napproach views information as the result of an observation process\ndr
iven by a sequential Mealy machine. In contrast\, the second approach\nfea
tures indistinguishability relations described by synchronous\ntwo-tape au
tomata.\n\nThe indistinguishability-relation model turns out to be strictl
y more\nexpressive than the one based on observations. We present a\nchara
cterisation of the indistinguishability relations that admit a\nrepresenta
tion as a finite-state observation function. We show that the\ncharacteris
ation is decidable\, and give a procedure to construct a\ncorresponding Me
aly machine whenever one exists.\n\nThe talk is based on joint work with D
ietmar Berwanger.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Checking Robustness Between Weak Transactional Consistency Models
- Sidi Mohamed Beillahi\, IRIF
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210517T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210517T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1389
DESCRIPTION:Concurrent accesses to databases are typically encapsulated in
transactions\nin order to enable isolation from other concurrent computat
ions and\nresilience to failures. Modern databases provide transactions wi
th various\nsemantics corresponding to different trade-offs between consis
tency and\navailability. Since a weaker consistency model provides better
performance\,\nan important issue is investigating the weakest level of c
onsistency\nneeded by a given program (to satisfy its specification).\nAs
a way of dealing with this issue\, we investigate the problem of checking\
nwhether a given program has the same set of behaviors when replacing a\nc
onsistency model with a weaker one.\nThis property known as robustness gen
erally implies that any specification\nof the program is preserved when we
akening the consistency. We focus on the\nrobustness problem for consisten
cy models which are weaker than standard\nserializability\, namely\, causa
l consistency\, prefix consistency\, and\nsnapshot isolation. We show tha
t checking robustness between these models\nis polynomial time reducible t
o a state reachability problem under\nserializability. We use this reducti
on to also derive a pragmatic proof\ntechnique based on Lipton's reduction
theory that allows to prove programs\nrobust. We have applied our techniq
ues to several challenging applications\ndrawn from the literature of dist
ributed systems and databases.\n\nThis a joint work with Ahmed Bouajjani a
nd Constantin Enea.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Foundational Aspects of the Blockchain Consensus - Bernadette Char
ron-Bost\, LIX\, École Polytechnique
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210607T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210607T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1410
DESCRIPTION:Decentralized cryptocurrencies such as Bitcoin have ignited mu
ch excitement\, not only for their novel realization of central bank-free
financial instruments\, but also as an alternative approach for the develo
pment of numerous distributed applications in which agreement must be reac
hed without central control and despite misbehaving parties. The soundness
and security of these applications\, however\, hinge on the thorough unde
rstanding of the fundamental properties of their underlying blockchain dat
a structure that parties (“miners”) maintain and try to extend by gene
rating “proofs of work”.\n\nIn this talk we formulate such fundamental
properties of the blockchain ---"common prefix"\, "chain quality"\, "chai
n growth"--- and show how the blockchain consensus differs from the classi
cal problem of consensus in distributed computing and from the consensus i
n control theory. We analyze the impact of different setups\, computationa
l assumptions\, and network models on the various properties of the blockc
hain consensus. We also examine the crucial role of the “proofs of work
” for achieving network synchrony on top of unstructured P2P networks.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:Reachability in Distributed Memory Automata - Arnaud Sangnier\, IR
IF\, Université de Paris
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210614T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210614T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1413
DESCRIPTION:We introduce Distributed Memory Automata\, a model of register
automata \nsuitable to capture some features of distributed algorithms de
signed for \nshared memory systems. In this model\, each participant owns
a local \nregister and a shared register and has the ability to change its
local \nvalue\, to write it in the global memory and to test atomically t
he \nnumber of occurrences of its value in the shared memory\, up to some
\nthreshold. We show that the control state reachability problem for \nDis
tributed Memory Automata is Pspace-complete for a fixed number of \npartic
ipants and is in Pspace when the number of participants is not \nfixed a p
riori.\n\nThis is a joint work with Benedikt Bollig and Fedor Ryabinin.
LOCATION:3052 and [[https://bbb-front.math.univ-paris-diderot.fr/recherche
/ber-rxi-tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:On Some Transducer Synthesis Problems - Emmanuel Filiot\, Universi
té Libre de Bruxelles
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210628T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210628T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1421
DESCRIPTION:The seminal Büchi-Landweber theorem states that reactive synt
hesis from\nomega-automatic specifications is decidable\, or equivalently\
, the synthesis\nproblem from specifications given by non-deterministic sy
nchronous (aka\nletter-to-letter) transducers. Moreover\, when such a spe
cification is\nrealizable\, it is realizable by a deterministic synchronou
s transducer. In\nthis talk\, we consider variants and generalizations of
this problem\, on\nfinite and infinite words\, where the synchronicity ass
umption is relaxed on\nthe specification side and/or the implementation si
de.
LOCATION:[[https://bbb-front.math.univ-paris-diderot.fr/recherche/ber-rxi-
tol-i7y|BBB link]]
END:VEVENT
BEGIN:VEVENT
SUMMARY:On the complexity of timed pattern matching - Eugène Asarin\, IRI
F\, Université de Paris
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20210705T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20210705T120000
DTSTAMP;VALUE=DATE-TIME:20210731T070300Z
UID:1423
DESCRIPTION:(joint work with Thomas Ferrère\, Dejan Nickovic and Dogan Ul
us)\n\nTimed pattern matching consists in finding occurrences of a timed r
egular expression in a timed word. This problem has been addressed using s
everal techniques\, its solutions are implemented in tools (quite efficien
t in practice)\, and used\, for example in log analysis and runtime verifi
cation. In this work\, we explore computational complexity of timed patte
rn matching\, and prove P\, NP and PSPACE bounds\, depending on connective
s used in expressions and other details. We conclude with a couple of open
questions.
LOCATION:3052 and [[https://bbb-front.math.univ-paris-diderot.fr/recherche
/ber-rxi-tol-i7y|BBB link]]
END:VEVENT
END:VCALENDAR