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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:TBA - Jules Villard\, Facebook
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20191216T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20191216T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110300Z
UID:932
DESCRIPTION:
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:20191207T110300Z
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:TBA - James Worrell\, University of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200224T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200224T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110300Z
UID:1027
DESCRIPTION:
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:20191207T110300Z
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:TBA - Pascale Gourdeau\, University of Oxford
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200302T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200302T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110300Z
UID:1029
DESCRIPTION:
LOCATION:Salle 1007
END:VEVENT
BEGIN:VEVENT
SUMMARY:TBA - David Monniaux\, University of Grenoble.
DTSTART;TZID=Europe/Paris;VALUE=DATE-TIME:20200210T110000
DTEND;TZID=Europe/Paris;VALUE=DATE-TIME:20200210T120000
DTSTAMP;VALUE=DATE-TIME:20191207T110300Z
UID:1030
DESCRIPTION:
LOCATION:Salle 1007
END:VEVENT
END:VCALENDAR