BEGIN:VCALENDAR
VERSION:2.0
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:Events at LSV
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:19700329T020000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:19701025T030000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
SUMMARY:
PhD Defense: Patrick Gardy
STATUS:CONFIRMED
DESCRIPTION:
Semantics of Strategy Logic Monday\, 12 June 2017 at 2:00pm
Pavillon des Jardins\, ENS Paris-Saclay
DTSTART;TZID=Europe/Paris:20170612T140000
DURATION:PT2H
URL;VALUE=URI:http://www.lsv.fr/~gardy/Defense/PhDDefense.php
UID:LSVGardyPhD@lsv.ens-cachan.fr
LOCATION:ENS Paris-Saclay (France)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
PhD Defense: Amina Doumane
STATUS:CONFIRMED
DESCRIPTION:
On the infinitary proof theory of logics with fixed points
Tuesday\, 27 June 2017 at 10:00am Université Paris-Diderot\,
Olympe-de-Gouges building\, room 255
DTSTART;TZID=Europe/Paris:20170627T100000
DURATION:PT2H
URL;VALUE=URI:https://www.irif.fr/~doumane/defense.htm
UID:LSVAminaPhD@lsv.ens-cachan.fr
LOCATION:Université Paris-Diderot (France)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
PhD Defense: David Montoya
STATUS:CONFIRMED
DESCRIPTION:
A personal knowledge base integrating user data and an acti
vity timeline Monday\, 6 March 2017 at 2pm Pavillon des Jard
ins\, ENS Cachan
DTSTART;TZID=Europe/Paris:20170306T140000
DURATION:PT2H
URL;VALUE=URI:https://montoya.one/talk/phd-defense/
UID:LSVMontoyaPhD@lsv.ens-cachan.fr
LOCATION:ENS Cachan (France)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
PhD Defense: Simon Theissing
STATUS:CONFIRMED
DESCRIPTION:
Supervision in Multimodal Transportation Systems Monday\, 5
December 2016 at 2pm Amphi Condorcet\, ENS Cachan
DTSTART;TZID=Europe/Paris:20161205T140000
DURATION:PT2H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/~theissing/defence.php
UID:LSVSimonPhD@lsv.ens-cachan.fr
LOCATION:ENS Cachan (France)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
PhD Defense: Pierre Halmagrand
STATUS:CONFIRMED
DESCRIPTION:
Automated Deduction and Proof Certification for the B Metho
d Saturday\, 10 December 2016 at 2pm CNAM\, Amphithéâtre Abb
é-Grégoire 292 rue Saint-Martin\, 75003 Paris
DTSTART;TZID=Europe/Paris:20161210T140000
DURATION:PT2H
URL;VALUE=URI:http://halmagrand.com/defense.html
UID:LSVPierreHPhD@lsv.ens-cachan.fr
LOCATION:Paris (France)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
3rd Saclay Seminar on Formal Methods - SASEFOR3
STATUS:CONFIRMED
DESCRIPTION:
The third SASEFOR meeting will take place at LRI (building 6
60's amphitheater) on November 24th\, 2015
DTSTART;VALUE=DATE:20151124
DURATION:P1D
URL;VALUE=URI:http://labex-digicosme.fr/GT+Methodes+Formelles
UID:LSVsasefor3@lsv.ens-cachan.fr
LOCATION:LRI\, Amphi bat. 660
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Habilitation Defense: Benedikt Bollig
STATUS:CONFIRMED
DESCRIPTION:
Automata and Logics for Concurrent Systems: Realizability a
nd Verification Tuesday 2 June 2015\, at 2pm Conference room
\, Pavillon des Jardins\, ENS Cachan
DTSTART;TZID=Europe/Paris:20150602T140000
DURATION:PT2H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/~bollig/
UID:LSVBenediktHDR@lsv.ens-cachan.fr
LOCATION:ENS Cachan (France)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
PhD Defense: Rémy Chrétien
STATUS:CONFIRMED
DESCRIPTION:
Automated analysis of equivalence properties for cryptograp
hic protocols Monday\, 11 January 2016 at 2pm Pavillon des J
ardins\, ENS Cachan
DTSTART;TZID=Europe/Paris:20160111T140000
DURATION:PT2H
URL;VALUE=URI:http://www.lsv.fr/~chretien/soutenance.php
UID:LSVRemyPhD@lsv.ens-cachan.fr
LOCATION:ENS Cachan (France)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
PhD Defense: Aiswarya Cyriac
STATUS:CONFIRMED
DESCRIPTION:
Verification of Communicating Recursive Programs via Split-
width Tuesday\, 28 January 2014\, at 2pm Pavillon des Jardin
s\, ENS Cachan
DTSTART;TZID=Europe/Paris:20140128T140000
DURATION:PT2H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/~cyriac/defense.php
UID:LSVAiswaryaPhD@lsv.ens-cachan.fr
LOCATION:ENS Cachan (France)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
PhD Defense: Romain Soulat
STATUS:CONFIRMED
DESCRIPTION:
Synthesis of Correct-by-Design Schedulers for Hybrid System
s Tuesday\, 18 February 2014\, at 2pm ENS Cachan\, Pavillon
des Jardins
DTSTART;TZID=Europe/Paris:20140218T140000
DURATION:PT2H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/~soulat/
UID:LSVSoulatPhD@lsv.ens-cachan.fr
LOCATION:ENS Cachan\, Pavillon des Jardins
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Habilitation Defense: Stefan Schwoon
STATUS:CONFIRMED
DESCRIPTION:
Efficient verification of sequential and concurrent systems
Friday\, December 6th 2013\, at 2pm Pavillon des Jardins\,
ENS Cachan
DTSTART;TZID=Europe/Paris:20131206T140000
DURATION:PT2H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/~schwoon/HDR.php
UID:LSVSchwoonHDR@lsv.ens-cachan.fr
LOCATION:ENS Cachan (France)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
PhD Defense: César Rodríguez
STATUS:CONFIRMED
DESCRIPTION:
Verification Based on Unfoldings of Petri Nets with Read Ar
cs Thursday\, December 12th 2013\, at 2pm Tocqueville lectur
e hall\, ENS Cachan
DTSTART;TZID=Europe/Paris:20131212T140000
DURATION:PT2H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/~rodriguez/defense.php
UID:LSVRodriguezPhD@lsv.ens-cachan.fr
LOCATION:ENS Cachan (France)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Habilitation Defense: Thomas Chatain
STATUS:CONFIRMED
DESCRIPTION:
Concurrency in Real-Time Distributed Systems\, from Unfoldi
ngs to Implementability Friday\, December 13th 2013\, at 2pm
Auditorium Daniel Chemla\, ENS Cachan
DTSTART;TZID=Europe/Paris:20131213T140000
DURATION:PT2H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/~chatain/HDR.php
UID:LSVChatainHDR@lsv.ens-cachan.fr
LOCATION:ENS Cachan (France)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
TBA
STATUS:CONFIRMED
ATTENDEE;CN="Dietrich Kuske
":
MAILTO:no@spam.com
DESCRIPTION:
DTSTART;TZID=Europe/Paris:20171003T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201710031
100
UID:LSVsemLSV.201710031100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
TBA
STATUS:CONFIRMED
ATTENDEE;CN="Josef Widder
":
MAILTO:no@spam.com
DESCRIPTION:
DTSTART;TZID=Europe/Paris:20170718T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201707181
100
UID:LSVsemLSV.201707181100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
TBA
STATUS:CONFIRMED
ATTENDEE;CN="Raul Fervari
":
MAILTO:no@spam.com
DESCRIPTION:
DTSTART;TZID=Europe/Paris:20170711T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201707111
100
UID:LSVsemLSV.201707111100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Improving Type Error Localization for Languages with Type In
ference
STATUS:CONFIRMED
ATTENDEE;CN="Thomas Wies
":
MAILTO:no@spam.com
DESCRIPTION:
Static type inference as found in programming languages such
as OCaml and Haskell is a prime example of a language featu
re that can boost productivity but that can also be a usabil
ity nightmare. A type inference algorithm infers the types o
f expressions in a program based on how these expressions ar
e used. The compiler can then use the inferred types to prov
e strong static correctness guarantees about a program witho
ut requiring any explicit type annotations. On the other han
d\, automated type inference can also be counterproductive.
If a conflicting use of an expression (i.e. a type mismatch)
is detected\, the compiler reports the corresponding progra
m location as the source of the type error. However\, the ac
tual error source is often elsewhere in the program. This ca
n result in confusing error messages. The programmer needs t
o understand the basic workings of the inference algorithm t
o interpret the error message correctly and debug the progra
m. This debugging process is often laborious and the lack of
better error localization steepens the learning curve for p
rogrammers learning the language. In this talk\, I will pres
ent a new algorithm for localizing type errors that provides
formal quality guarantees about the identified type error s
ources. The algorithm works efficiently in practice and has
the potential to significantly improve the quality of type e
rror reports produced by state-of-the-art compilers.
DTSTART;TZID=Europe/Paris:20170627T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201706271
100
UID:LSVsemLSV.201706271100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Quantum Digital Physics?
STATUS:CONFIRMED
ATTENDEE;CN="Pablo Arrighi
":
MAILTO:no@spam.com
DESCRIPTION:
The 60's 'Digital Physics' program advocates that space may
be nothing but a grid\, with each cell containing a bounded
amount of bits of information\, and the whole thing evolvin
g in discrete time steps according to a local rule. Thus acc
ording to this somewhat reductionist view the universe is bu
t a cellular automaton. At least two things are wrong with t
his picture. First\, general relativity tells us that the sp
ace should at least be a graph\, and that this graph should
evolve under the local rule. Second\, quantum theory tells u
s that the graph may well evolve into a quantum superpositio
n of graphs\, and that this overall evolution should be unit
ary. This suggests a 2020's 'Quantum Digital Physics' progra
m modelling space as superpostions of graphs\, and time-evol
ution as a unitary causal operator. A theorem shows that suc
h time-evolutions take the form of a quantum circuit of fini
te depth.
DTSTART;TZID=Europe/Paris:20170620T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201706201
100
UID:LSVsemLSV.201706201100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
A Curry-Howard Approach to Tree Automata
STATUS:CONFIRMED
ATTENDEE;CN="Colin Riba
":
MAILTO:no@spam.com
DESCRIPTION:
This talk surveys a Curry-Howard perspective on Rabin's Tree
Theorem\, the decidability of Monadic Second-Order Logic (M
SO) on infinite trees. Rabin's Tree Theorem proceeds by effe
ctive translations of MSO-formulae to tree automata. The ope
rations on tree automata used in these translations can be o
rganized in a deduction system based on intuitionistic linea
r logic (ILL). We propose a computational interpretation of
this deduction system along the lines of the Curry-Howard pr
oofs-as-programs correspondence. Relying on the usual techno
logy of game semantics\, we interpret proofs as strategies i
n two-player games generalizing usual acceptance games of tr
ee automata. This realizability semantics satisfies an expec
ted property of witness extraction from proofs of existentia
l statements. It also allows to combine realizers produced a
s interpretations of proofs with strategies witnessing (non-
)emptiness of tree automata\, possibly obtained using extern
al algorithms. Moreover\, an adaptation of a usual construct
ion for the simulation of alternating automata by non-determ
inistic ones satisfies the deduction rules of the "of course
" exponential modality of ILL.
DTSTART;TZID=Europe/Paris:20170613T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201706131
100
UID:LSVsemLSV.201706131100@lsv.ens-cachan.fr
LOCATION:Auditorium Daniel Chemla (Bât. Institut D'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Some optimization problems in networks
STATUS:CONFIRMED
ATTENDEE;CN="Nelson Maculan
":
MAILTO:no@spam.com
DESCRIPTION:
We present optimization models with a polynomial number of v
ariables and constraints for combinatorial optimization prob
lems in networks: optimum elementary cycles (whose traveling
salesman problem)\, optimum elementary paths even in a grap
h with negative cycles\, and optimum trees (whose Steiner tr
ee problem) problems. Computational results for the Steiner
tree problem are also presented.
DTSTART;TZID=Europe/Paris:20170516T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201705161
100
UID:LSVsemLSV.201705161100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
BINSEC: Binary-level Semantic Analysis to the Rescue
STATUS:CONFIRMED
ATTENDEE;CN="Sébastien Bardin
":
MAILTO:no@spam.com
DESCRIPTION:
Several major classes of security analysis have to be perfo
rmed on raw executable files\, such as vulnerability analysi
s of mobile code or commercial off-the-shelf\, deobfuscation
or malware inspection. These analysis are very challenging\
, due to the very low-level and intricate nature of binary c
ode\, and they are still relatively poorly tooled -- essenti
ally syntactic static analysis (disassembly) which is easy t
o fool\, or dynamic analysis (fuzzing\, monitoring) which ma
y miss subtle behaviors. On the other hand\, source-level pr
ogram analysis and formal methods have made tremendous progr
ess in the past decade\, and they are now an industrial real
ity for safety-critical applications. The open-source BINSEC
platform humbly tries to fulfill part of this gap\, by prov
iding state-of-the-art binary-level semantic analyses. The p
latform is built around a concise and generic Intermediate R
epresentation\, making it easy to support new architectures
and add new analyses. The main analyses so far include a dyn
amic symbolic execution engine enabling to discover new subt
le behaviors in an executable file\, and a semantic static a
nalysis engine able to reason about all paths of a portion o
f the code under analysis. In this this talk\, we will prese
nt the benefits & challenges of binary-level formal methods
as well as the BINSEC platform and the underlying key techno
logies\, through a few examples taken from deobfuscation and
vulnerability analysis.
DTSTART;TZID=Europe/Paris:20170502T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201705021
100
UID:LSVsemLSV.201705021100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Hybrid realizability for intuitionistic and classical choice
STATUS:CONFIRMED
ATTENDEE;CN="Valentin Blot
":
MAILTO:no@spam.com
DESCRIPTION:
The axiom of choice is ubiquitous in mathematics\, and its c
omputational interpretation is an important step towards cer
tification of a wide range of programs. However\, this compu
tational content is highly dependent on whether we work in c
lassical or in intuitionistic logic (with or without the exc
luded middle). Indeed\, while in an intuitionistic setting t
he axiom of choice can be interpreted with a simple and pure
ly functional program\, its interpretation in the classical
case requires strong recursion schemes like bar recursion. T
his complexity does not come as a surprise since the combina
tion of the axiom of choice with classical logic proves the
existence of non- computable functions. I will present a hyb
rid system encompassing both the classical and intuitionisti
c settings\, where both intuitionistic and classical choice
are interpreted with their usual respective realizers. This
model relies on a notion of polarity on formulas that keeps
track of the uses of classical logic in a proof.
DTSTART;TZID=Europe/Paris:20170418T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201704181
100
UID:LSVsemLSV.201704181100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Runtime Analysis of Randomized Algorithms: A Dijkstra Déjà V
u
STATUS:CONFIRMED
ATTENDEE;CN="Joost-Pieter Katoen
":
MAILTO:no@spam.com
DESCRIPTION:
Randomization is an important tool in algorithm design for o
btaining efficient solutions; e.g.\, random pivot selection
in quicksort lowers the expected runtime (ER) to O(n log n).
Reasoning about the ER of randomized algorithms is subtle a
nd full of nuances\, as: they may have diverging runs but ha
ve a finite ER; they may almost surely terminate but have an
infinite ER; running two finite-ER algorithms in sequence m
ay yield an infinite ER. ER analysis of randomized algorithm
s is typically done using classical probability theory\, mos
tly with arguments relying on random variable expectations o
r martingales. These analyses partially follow an ad-hoc rea
soning and take non-trivial relationships between random var
iables for granted. In this talk\, I'll present a formal ver
ification approach towards the ER analysis using a weakest-p
recondition approach Ã la Dijkstra. It allows e.g. to prove
the positive almost-sure termination: does a program termin
ate with probability one in finite expected time? We show pr
oof rules for loops prove the soundness w.r.t a simple opera
tional mode and argue that our approach conservatively exten
ds Nielson's approach for deterministic programs.
DTSTART;TZID=Europe/Paris:20170329T100000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201703291
000
UID:LSVsemLSV.201703291000@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
A formal set-theoretical model of Coq and its application to
strong normalization
STATUS:CONFIRMED
ATTENDEE;CN="Bruno Barras
":
MAILTO:no@spam.com
DESCRIPTION:
I will describe the formalization in Coq of two crucial met
atheoretical properties of the formalism of the Coq proof as
sistant: consistency and strong normalization (SN). While it
is clear why we prove the consistency of a logical formalis
m\, I will give a motivation for the SN property. Of course\
, as Gödel showed\, proving the consistency of a formalism i
n itself is only proving it is inconsistent. The usual way o
ut is to make Coq stronger by adding axioms. In our case\, w
e have extended Coq to make it as strong as intuitionistic s
et-theory with Grothendieck universes (an intuitionistic cou
nterpart of inaccessible cardinals). Then\, I will sketch an
intuitive translation from the Calculus of Inductive Constr
uctions (the formalism of Coq) to set theory\, and prove tha
t this interpretation is sound. The difficult part is to int
erpret inductive types. As a reward\, we derive the consiste
ncy of Coq relative to the set theory described above. Using
a slight variant of the set-theoretical interpretation\, I
will explain how to build a strong normalization model\, whi
ch soundness implies the SN property. The remarkable feature
of this model is that it is very modular: the complexity of
inductive types have been broken into simpler principles.
DTSTART;TZID=Europe/Paris:20170328T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201703281
100
UID:LSVsemLSV.201703281100@lsv.ens-cachan.fr
LOCATION:Auditorium Daniel Chemla (Bât. Institut D'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Asynchronous Distributed Automata: A Characterization of the
Modal Mu-Fragment
STATUS:CONFIRMED
ATTENDEE;CN="Fabian Reiter
":
MAILTO:no@spam.com
DESCRIPTION:
I will present the equivalence between a class of asynchrono
us distributed automata and a small fragment of least fixpoi
nt logic\, when restricted to finite directed graphs. More s
pecifically\, the considered logic is (a variant of) the fra
gment of modal Î¼-calculus that allows least fixpoints but f
orbids greatest fixpoints. The corresponding automaton model
uses a network of identical finite-state machines that comm
unicate in an asynchronous manner and whose state diagram mu
st be acyclic except for self-loops. As a by-product\, the c
onnection with logic also entails that the expressive power
of those machines is independent of whether or not messages
can be lost.
DTSTART;TZID=Europe/Paris:20170221T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201702211
100
UID:LSVsemLSV.201702211100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Reduction and reversal of discrete models of biological regu
latory networks
STATUS:CONFIRMED
ATTENDEE;CN="Aurélien Naldi
":
MAILTO:no@spam.com
DESCRIPTION:
Logical (discrete: Boolean or multivalued) models have been
used to study biological regulatory networks over the last 4
0 years. The increasing size of the networks of interest cal
ls for formal methods for their dynamical analysis. We propo
sed a model reduction method\, to construct "simpler" versio
n of the models by taking out selected components and integr
ating their role in the functions of their targets. We showe
d that this rewiring of the model is only possible for compo
nents which are not self-regulated\, and that this condition
ensures the preservation of the attractors. While this redu
ction can not create additional reachability properties\, it
can\, in case of conflicts\, remove some of the existing on
es. To study the basins of attraction\, we propose the const
ruction of a "reversed" model regarding the asynchronous dyn
amical behaviour: the successors of the states of a reversed
model correspond to their predecessors in the original one.
While the reversal can be generalized only to a particular
class of multivalued models\, we show how to use model boole
anization to study the reversed asynchronous dynamics of any
model. The study of the reversed dynamics then facilitates
the identification of the basins of attraction\, assuming th
at we already know the attractors. We can further compute "s
trong" and "weak" basins (from which we can respectively rea
ch a unique or multiple attractors)\, as well as their "fron
tiers"\, i.e.\, the sets of states such that the reachable a
ttractors are different from the attractors reachable from n
eighbouring states (predecessors or successors)
DTSTART;TZID=Europe/Paris:20170207T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201702071
100
UID:LSVsemLSV.201702071100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
A Model Checking Approach to Dynamical Systems Analysis
STATUS:CONFIRMED
ATTENDEE;CN="David Safranek
":
MAILTO:no@spam.com
DESCRIPTION:
We will describe our novel high-performance algorithm for sy
nthesis of interdependent parameters from CTL specifications
for non-linear dynamical systems based on coloured model ch
ecking. The method employs a symbolic representation of sets
of parameter valuations in terms of first-order theory of t
he reals. Moreover\, we will discuss an interesting extensio
n of the algorithm that allows to address the problem of bif
urcation analysis of parameterised high-dimensional dynamica
l systems. To this end\, we introduce the hybrid CTL logic a
ugmented with direction formulae. This allows us to describe
various behaviour patterns and phase portraits. Finally\, w
e will describe applications of the method to a class of pie
cewise multi-affine dynamical systems representing dynamics
of biological systems with complex non-linear behaviour invo
lving multi-stability or limit cycles.
DTSTART;TZID=Europe/Paris:20170124T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201701241
100
UID:LSVsemLSV.201701241100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Why liveness for timed automata is hard and what we can do a
bout it
STATUS:CONFIRMED
ATTENDEE;CN="B Srivathsan
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk\, we will show that if P is not equal to NP\, t
he liveness problem for timed automata is more difficult tha
n the reachability problem. We will then present a new algor
ithm to solve the liveness problem for timed automata\, and
compare it with existing solutions. Joint work with F. Herbr
eteau\, T.T Tran and I. Walukiewicz.
DTSTART;TZID=Europe/Paris:20170117T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201701171
100
UID:LSVsemLSV.201701171100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Biabduction (and Related Problems) in Array Separation Logic
STATUS:CONFIRMED
ATTENDEE;CN="Nikos Gorogiannis
":
MAILTO:no@spam.com
DESCRIPTION:
We investigate Array Separation Logic\, a variant of symboli
c-heap separation logic in which the primary data structures
are not pointers or lists but arrays. This logic can be use
d for proving memory safety for array-manipulating imperativ
e programs. We focus on the biabduction problem for this log
ic\, which has been established as the key to automatic spec
ification inference at the industrial scale in the setting o
f standard separation logic. Specifically\, we show that the
problem of finding a solution is NP-complete\, and we prese
nt a concrete NP algorithm for biabduction that produces sol
utions of reasonable quality. Along the way\, we show that s
atisfiability in our logic is NP-complete\, and that entailm
ent is decidable with high complexity. The somewhat surprisi
ng fact that biabduction is computationally simpler than ent
ailment is explained by the fact that\, as we show\, the ele
ment of choice over biabduction solutions enables us to dram
atically reduce the search space.
DTSTART;TZID=Europe/Paris:20161206T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201612061
100
UID:LSVsemLSV.201612061100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Proving Differential Privacy via Probabilistic Couplings
STATUS:CONFIRMED
ATTENDEE;CN="Pierre-Yves Strub
":
MAILTO:no@spam.com
DESCRIPTION:
Differential privacy is a promising formal approach to data
privacy\, which provides a quantitative bound on the privacy
cost of an algorithm that operates on sensitive information
. Several tools have been developed for the formal verificat
ion of differentially private algorithms\, including program
logics and type systems. However\, these tools do not captu
re fundamental techniques that have emerged in recent years\
, and cannot be used for reasoning about cutting-edge differ
entially private algorithms. Existing techniques fail to han
dle three broad classes of algorithms: 1) algorithms where p
rivacy de- pends on accuracy guarantees\, 2) algorithms that
are analyzed with the advanced composition theorem\, which
shows slower growth in the privacy cost\, 3) algorithms that
interactively accept adaptive inputs. In this presentation\
, I will develop compositional methods for formally verifyin
g differential privacy for algorithms whose analysis goes be
yond the composition theorem. The methods are based on the o
bservation that differential privacy has deep connections wi
th a generalization of probabilistic couplings\, an establis
hed mathematical tool for reasoning about stochastic process
es. Even when the composition theorem is not helpful\, we ca
n often prove privacy by a coupling argument. I will illustr
ate this approach through a single running example\, which e
xemplifies the three classes of algorithms and explores new
variants of the Sparse Vector technique\, a well-studied alg
orithm from the privacy literature.
DTSTART;TZID=Europe/Paris:20161122T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201611221
100
UID:LSVsemLSV.201611221100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Kripke Semantics and Uniformity for Type Theory with constra
ints
STATUS:CONFIRMED
ATTENDEE;CN="Jim Lipton
":
MAILTO:no@spam.com
DESCRIPTION:
We will start by giving a presentation of type theory (Churc
h + Intuitionistic) with embedded constraints. We follow wit
h a modified calculus suitable for logic programming. In ord
er to prove the two systems equivalent semantically for the
case of Program |- Goal sequents we develop two different no
tions of Kripke Model for each of the two systems. We then s
how they are sound and complete for each calculus respective
ly. The two semantics are then compared to give a semantic p
roof of the equivalence mentioned above.
DTSTART;TZID=Europe/Paris:20161115T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201611151
100
UID:LSVsemLSV.201611151100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Opacity for Linear Constraint Markov Chains
STATUS:CONFIRMED
ATTENDEE;CN="Béatrice Bérard
":
MAILTO:no@spam.com
DESCRIPTION:
On a partially observed system\, a secret Ï is opaque if an
observer cannot ascertain that its trace belongs to Ï. We
consider specifications given as Constraint Markov Chains (C
MC)\, which are underspecified Markov chains where probabili
ties on edges are required to belong to some set. The nondet
erminism is resolved by a scheduler\, and opacity on this mo
del is defined by disclosure\, a worst case measure over all
implementations obtained by scheduling. Hence disclosure me
asures the information obtained by a passive observer when t
he system is controlled by the smartest scheduler in coaliti
on with the observer. When restricting to the subclass of Li
near CMC\, we compute (or approximate) this measure and prov
e that refinement of a specification can only improve opacit
y. Joint work with Olga Kouchnarenko\, John Mullins and Math
ieu Sassolas\, extended version from WODES 2016.
DTSTART;TZID=Europe/Paris:20161108T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201611081
100
UID:LSVsemLSV.201611081100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Highly restricted distributed systems - the example of opini
on dynamics
STATUS:CONFIRMED
ATTENDEE;CN="Matthias Fuegger
":
MAILTO:no@spam.com
DESCRIPTION:
Several man-made distributed systems\, like mobile sensor no
des\, and natural distributed systems\, like bird flocks\, c
an be modeled by agents whose communication or computational
capabilities are severely limited. I will start with a brie
f overview on problems I have been and am currently looking
at within this domain\, ranging from VLSI systems to the Phy
sarum slime mold. The main part of the talk will then detail
on a prominent example from opinion dynamics: so called Heg
selmann-Krause (HK) systems. Although its update rules are d
eceptively simple\, many fundamental questions are still ope
n today. I will give an introduction into the state of the a
rt about HK\, discuss different proof techniques\, and show
effective bounds on agent stabilization time. The talk concl
udes with a list of open problems.
DTSTART;TZID=Europe/Paris:20161025T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201610251
100
UID:LSVsemLSV.201610251100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Analyzing Timed Systems Using Tree Automata
STATUS:CONFIRMED
ATTENDEE;CN="Paul Gastin
":
MAILTO:no@spam.com
DESCRIPTION:
Timed systems\, such as timed automata\, are usually analyze
d using their operational semantics on timed words. The clas
sical region abstraction for timed automata reduces them to
(untimed) finite state automata with the same time-abstract
properties\, such as state reachability. We propose a new te
chnique to analyze such timed systems. The main idea is to c
onsider timed behaviors as graphs with matching edges captur
ing timing constraints. As an example\, we develop the techn
ique on timed pushdown systems. We show that their behaviors
are graphs of bounded tree-width. Hence\, they can be inter
preted in trees opening the way to tree automata based techn
iques which are more powerful than analysis based on word au
tomata. The technique is quite general and applies to many t
imed systems. Joint work with S. Akshay and Shankar Narayana
n Krishna from IIT Bombay\, extended abstract at CONCUR'16.
DTSTART;TZID=Europe/Paris:20161004T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201610041
100
UID:LSVsemLSV.201610041100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Knowledge\, Action and Communication
STATUS:CONFIRMED
ATTENDEE;CN="Yoram Moses
":
MAILTO:no@spam.com
DESCRIPTION:
Decisions taken by an agent in a multi-agent system depend o
n the agent's local information. A new formulation of the co
nnection between knowledge and action in multi-agent systems
allows new insights into the design of such systems. The fi
rst part of this talk will relate knowledge to coordinated a
ction in a multi-agent setting. The second part of the talk
will use the observations made in the first part to capture
the role of time and timing information in coordinating acti
ons in systems with clocks. While message chains play a domi
nant role in asynchronous systems\, a corresponding notion i
s established for systems with clocks and time bounds on mes
sage delivery. The second part is based on joint work with I
do Ben Zvi.
DTSTART;TZID=Europe/Paris:20160913T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201609131
100
UID:LSVsemLSV.201609131100@lsv.ens-cachan.fr
LOCATION:Auditorium Daniel Chemla (Bât. Institut D'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Recency-Bounded Verification of Dynamic Database-Driven Syst
ems
STATUS:CONFIRMED
ATTENDEE;CN="Aiswarya Cyriac
":
MAILTO:no@spam.com
DESCRIPTION:
We propose a formalism to model database-driven systems\, ca
lled database manipulating systems (DMS). The actions of a D
MS modify the current instance of a relational database by a
dding new elements into the database\, deleting tuples from
the relations and adding tuples to the relations. The elemen
ts which are modified by an action are chosen by (full) firs
t-order queries. DMS is a highly expressive model and can be
thought of as a succinct representation of an infinite stat
e relational transition system\, in line with similar models
proposed in the literature. We propose monadic second order
logic (MSO-FO) to reason about sequences of database instan
ces appearing along a run. Unsurprisingly\, the linear-time
model checking problem of DMS against MSO-FO is undecidable.
Towards decidability\, we propose under-approximate model c
hecking of DMS\, where the under-approximation parameter is
the âbound on recencyâ. In a k-recency-bounded run\, onl
y the most recent k elements in the current active domain ma
y be modified by an action. More runs can be verified by inc
reasing the bound on recency. Our main result shows that rec
ency-bounded model checking of DMS against MSO-FO is decidab
le\, by a reduction to the satisfiability problem of MSO ove
r nested words. This is a joint work with Parosh Abdulla\, M
ohammed Faouzi Atig\, Marco Montali and Othmane Rezine.
DTSTART;TZID=Europe/Paris:20160621T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201606211
100
UID:LSVsemLSV.201606211100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Sharing the Burden of (Dis)proof with Automatic Tools
STATUS:CONFIRMED
ATTENDEE;CN="Jasmin Blanchette
":
MAILTO:no@spam.com
DESCRIPTION:
The proof assistant Isabelle/HOL owes much of its success to
its ease of use and powerful automation. Much of the automa
tion is performed by external tools: The metaprover Sledgeha
mmer relies on external automatic theorem provers for its pr
oof search\, and the counterexample generator Nitpick is bas
ed on a finite model finder\, which performs a reduction to
propositional satisfiability (SAT). This talk will describe
how these tools work and how they help make Isabelle users m
ore productive.
DTSTART;TZID=Europe/Paris:20160614T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201606141
100
UID:LSVsemLSV.201606141100@lsv.ens-cachan.fr
LOCATION:Auditorium Daniel Chemla (Bât. Institut D'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Reachability problems for classical mathematical objects
STATUS:CONFIRMED
ATTENDEE;CN="Igor Potapov
":
MAILTO:no@spam.com
DESCRIPTION:
Reachability is a fundamental problem in the context of many
finite and infinite state systems\, computational models\,
hybrid and dynamical systems\, rewriting systems\, probabili
stic and parametric systems\, and open systems modelled as g
ames. In general terms\, it can be formalized as follows: fo
r a computation model specified via a set of allowed rules o
r transformations\, decide whether a certain state is reacha
ble from a given initial state. The proposed talk will be fo
cused on reachability problems for classical mathematical ob
jects\, which naturally appear in many computational process
es and abstractions. I will mainly focus on such objects as
words\, matrices\, iterative maps\, knots\, braids and will
aim to highlight most recent developments on decidability an
d complexity results in the area and will illustrate connect
ions of reachability questions with fundamental long standin
g open problems in mathematics and computer science.
DTSTART;TZID=Europe/Paris:20160517T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201605171
100
UID:LSVsemLSV.201605171100@lsv.ens-cachan.fr
LOCATION:Auditorium Daniel Chemla (Bât. Institut D'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Checking the floating point accuracy of scientific codes by
using the verificarlo tool
STATUS:CONFIRMED
ATTENDEE;CN="Christophe Denis
":
MAILTO:no@spam.com
DESCRIPTION:
In the next decade\, exascale supercomputers will provide th
e computational power required to perform very large scale s
imulations. For certain applications the results of exascale
simulations will be of such high reslution that experimenta
l measurements will be insufficient for validation purposes.
As floating point approximations of numeric expressions are
neither associative nor distributive\, the results of a num
erical simulation can differ between executions. As reported
by the numerician I. S. Duff\, "Getting different results f
or different runs of the same computation can be disconcerti
ng for users even if\, in a sense\, both results are correct
". There is a need to have an automatic and global approach
giving a confidence interval on the results taking into acco
unt the floating point arithmetic effect. The estimation of
the effect of the floating point model on the accuracy of th
e computed results is the first step of a rigorous Verificat
ion and Validation (V&V) procedure. This talk is organised a
s follows. The context of our work and in particular the dar
k side of the floating point computation is firstly presente
d. A brief overview of some numerical verification tools is
the reported. Then\, the new tool called verificarlo is expo
sed. Using verificarlo is transparent for the user and does
not require manually modifying the source code. It can be us
ed for the automatic assessment of the numerical accuracy of
large scale digital simulations by using the Monte-Carlo Ar
ithmetic. Several examples will be displayed in particular t
he numerical verification of the solving of linear systems u
sing the LAPACK and BLAS scientific libraries. More informat
ion about the verificarlo tool could be obtained here: https
://hal.archives-ouvertes.fr/hal-01192668
DTSTART;TZID=Europe/Paris:20160419T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201604191
100
UID:LSVsemLSV.201604191100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Analysing a corpus of legal decisions from a network-science
perspective
STATUS:CONFIRMED
ATTENDEE;CN="Fabien Tarissan
":
MAILTO:no@spam.com
DESCRIPTION:
As many real-world networks\, legal networks lend themselves
to the use of graphs in which nodes represent the decisions
and links stand for citations between decisions. This line
of research has proved to be efficient for detecting importa
nt decisions in legal rulings. Although useful\, this framew
ork does not account for the inherent complexity and hierarc
hy commonly observed in real data. In the context of legal n
etworks in particular\, interactions between decisions take
place at various levels\, inducing a two-level structure. I
propose here to rely on a hybrid version of bipartite graphs
\, which allows to represent different types of links in mul
ti-level networks. I assess the relevance of this approach b
y analysing the hybrid structure of the first cases of the I
nternational Criminal Court and by confronting it with stand
ard approaches focusing on direct citation processes. Finall
y\, I will show how to extend structural analyses with tempo
ral properties in order to refine the identification of impo
rtant decisions. I validate the outcomes by providing juridi
cal interpretations of the results.
DTSTART;TZID=Europe/Paris:20160405T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201604051
100
UID:LSVsemLSV.201604051100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Markovian modeling for information leakage quantification
STATUS:CONFIRMED
ATTENDEE;CN="Fabrizio Biondi
":
MAILTO:no@spam.com
DESCRIPTION:
Information leakage quantifies the amount of bits of informa
tion about a system's secret that is obtained by an attacker
able to observe the secret's output. It is common to model
a terminating system as a channel matrix and to compute leak
age as the mutual information between the input and output o
f the channel. Hovewer\, Markovian models can model systems
in a more concrete way\, considering the system's control fl
ow and in many cases producing a smaller model\, and can als
o model non-terminating systems. We will show how Markovian
models can be used to model a system's specification and to
synthesize the implementation with the highest leakage if it
exists. We will discuss leakage and leakage rate of non-ter
minating systems\, and we will show how the Markovian analys
is can be used to implement a fast leakage computation algor
ithm based on trace analysis\, currently implemented in the
state-of-the-art QUAIL tool. Slides available here.
DTSTART;TZID=Europe/Paris:20160329T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201603291
100
UID:LSVsemLSV.201603291100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Universality of Causal Graph Dynamics
STATUS:CONFIRMED
ATTENDEE;CN="Simon Martiel
":
MAILTO:no@spam.com
DESCRIPTION:
Causal Graph Dynamics generalize Cellular Automata\, extendi
ng them to bounded degree\, time varying graphs. The dynamic
s rewrite the graph at each time step with respect to two ph
ysics-like symmetries: causality (bounded speed of informati
on) and homogeneity (the rewriting acts the same everywhere
on the graph\, at every time step). Universality is the abil
ity of simulating every other instances of another (or the s
ame) model of computation. In this talk\, we will present di
fferent ways to achieve universality for the model of CGD. M
ore particularly\, we will present the construction of an in
trinsically universal and uniform family of CGD.
DTSTART;TZID=Europe/Paris:20160308T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201603081
100
UID:LSVsemLSV.201603081100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Verification of Quantum Cryptography
STATUS:CONFIRMED
ATTENDEE;CN="Dominique Unruh
":
MAILTO:no@spam.com
DESCRIPTION:
In recent years\, the verification of cryptographic schemes
on the computational level (i.e.\, without symbolic abstract
ions) has seen great progress. For example\, various state-o
f-the-art cryptographic schemes were analyzed using the Easy
Crypt tool using a probabilistic relational Hoare logic (pRH
L). However\, existing tools and logics are unsuited for ana
lysis of quantum cryptographic protocol - be it protocols us
ing quantum mechanics\, or protocols secure against quantum
adversaries. In this talk\, we explain why pRHL is not sound
for quantum cryptography\, and show how to lift the ideas f
rom pRHL to the quantum setting. (With the long-term goal of
getting a quantum version of EasyCrypt.)
DTSTART;TZID=Europe/Paris:20160112T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201601121
100
UID:LSVsemLSV.201601121100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Online Space Complexity
STATUS:CONFIRMED
ATTENDEE;CN="Nathanaël Fijalkow
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk\, I will speak about the Online Space Complexit
y of languages\, which is an old topic (studied by Karp\, Mi
nsky\, Hartmanis and others in the 60s) that I picked up rec
ently. The main question is the following: given a language
L\, how many states does an automaton need to recognise L\,
as a function of the input length? This question is well-und
erstood for regular languages\, which are those recognised b
y finite automata\, so we go beyond this case and study non-
regular languages. This talk will be a gentle introduction t
o these questions; I will present some results about the onl
ine space complexity of probabilistic languages. Based on a
forthcoming paper at LFCS'2016.
DTSTART;TZID=Europe/Paris:20151215T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201512151
100
UID:LSVsemLSV.201512151100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Proof complexity of deep inference: past\, present and futur
e
STATUS:CONFIRMED
ATTENDEE;CN="Anupam Das
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk I will survey the current state of research on
the complexity of deep inference proofs in classical proposi
tional logic\, and also introduce a program of research prop
osing to further develop this subject. Deep inference calcul
i\, due to Guglielmi and others\, differ from traditional sy
stems by allowing proof rules to operate on any connective o
ccurring in a formula\, as opposed to just the main connecti
ve. Consequently such calculi are more fine-grained and admi
t smaller proofs of benchmark tautologies\, including the pi
geonhole principle. As well as plainly theoretical motivatio
ns\, this is advantageous from the point of view of proof co
mmunication\, allowing for compact and easy-to-check certifi
cates for proofs. I present a graph-based formalism called '
atomic flows' and a rewriting system on them that models pro
of normalisation while preserving complexity properties. I s
how how such an abstraction has been influential in work up
to now\, allowing the obtention of surprisingly strong upper
bounds and simulations in analytic deep inference. The bigg
est open question in the area is the relative complexity bet
ween the minimal system KS and a version that allows a form
of sharing\, KS+. To this end I will introduce a novel appro
ach using weak fragments of arithmetic to serve as uniform c
ounterparts to these nonuniform propositional systems\, insp
ired by the approach of bounded arithmetic. As well as assoc
iating a propositional system with an arithmetic theory in a
formal sense\, this also naturally identifies an associated
complexity class of functions\, and so tools and intuitions
from logic and complexity theory can thence be used to obta
in more powerful results in proof complexity. Due to the pec
uliarities of deep inference calculi\, the search for corres
ponding arithmetic theories takes us into the unexplored ter
ritories (from the point of view of bounded arithmetic) of i
ntuitionistic and substructural logics\, requiring an intere
sting interplay of subjects at the interface of logic and co
mputation.
DTSTART;TZID=Europe/Paris:20151209T143000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201512091
430
UID:LSVsemLSV.201512091430@lsv.ens-cachan.fr
LOCATION:Amphi A 117 (Bat. Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
A symbolic control approach to the design of cyber-physical
systems
STATUS:CONFIRMED
ATTENDEE;CN="Antoine Girard
":
MAILTO:no@spam.com
DESCRIPTION:
Cyber-physical systems (CPS) consist of computational elemen
ts monitoring and controlling physical entities. Their devel
opment requires a deep understanding of the dynamics of the
physical process usually modeled by differential equations.
We present an approach aiming at helping CPS design and base
d on: 1) a high-level programming language allowing us to sp
ecify functionalities of the CPS while abstracting the detai
ls of the physical dynamics; 2) an automated model-based syn
thesis tool generating from a high-level program\, a low-lev
el controller implementing the specified functionalities. Th
e approach is based on the use of symbolic models (i.e. disc
rete abstractions) of the dynamics of the physical process a
nd follows the correct by construction synthesis paradigm. I
n this talk\, we will review our contributions to the field
of symbolic control and identify the challenges that need to
be addressed in future research.
DTSTART;TZID=Europe/Paris:20151208T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201512081
100
UID:LSVsemLSV.201512081100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Designing Location Privacy Mechanisms for flexibility over t
ime and space
STATUS:CONFIRMED
ATTENDEE;CN="Marco Stronati
":
MAILTO:no@spam.com
DESCRIPTION:
With the increasing popularity of GPS-enabled handheld devic
es\, location based services (LBS) have access to accurate l
ocation information\, raising serious privacy concerns for e
nd users. Trying to address these issues\, the notion of geo
-indistinguishability was recently introduced\, protecting p
rivacy by reporting to the LBS only a noisy version of the u
ser's location. Standard geo-indistinguishability works well
in the case of a sporadic use\, however\, under repeated us
e over time\, constantly applying noise leads to a quick los
s of privacy. In the first part of this thesis we show that
correlation in the trace can be in fact exploited through a
prediction function that tries to guess the new location red
ucing the number of sanitized positions. Another drawback of
geo-indistinguishability is that it treats space in a unifo
rm way\, imposing the addition of the same amount of noise e
verywhere on the map. In the second part of this thesis we p
ropose a novel elastic mechanism that adapts the level of no
ise to the different degrees of density of each area.
DTSTART;TZID=Europe/Paris:20151201T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201512011
100
UID:LSVsemLSV.201512011100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Seminar cancelled
STATUS:CONFIRMED
ATTENDEE;CN="Bruno Bouchard
":
MAILTO:no@spam.com
DESCRIPTION:
The seminar is cancelled.
DTSTART;TZID=Europe/Paris:20151117T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201511171
100
UID:LSVsemLSV.201511171100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Cross-fertilization of proof theory and automated theorem pr
oving : the case of resolution modulo theory
STATUS:CONFIRMED
ATTENDEE;CN="Guillaume Burel
":
MAILTO:no@spam.com
DESCRIPTION:
Deduction modulo theory is a framework in which an existing
proof system (e.g. the sequent calculus\, the lambda-Pi calc
ulus\, or resolution) is enriched with a congruence modulo w
hich the inference rules are applied. It was first introduce
d to prove the completeness of some automated theorem provin
g methods. In this talk\, we study how proof theory and auto
mated theorem proving both benefit from it. First\, the comp
leteness of the combination of two well-known refinements of
resolution\, namely ordered resolution and set-of-support s
trategy\, is shown to be equivalent to a proof theoretic pro
perty\, namely the admissibility of the cut rule in the sequ
ent calculus modulo theory. This ensures not only that provi
ng cut admissibility (for instance by proving strong normali
zation) implies the completeness of resolution modulo theory
; but also that we can use saturation techniques to obtain
a presentation of a theory that is suitable for deduction mo
dulo theory. Second\, this link can be used to embed resolut
ion modulo theory into an existing automated theorem prover
based on resolution\, such as iProver. Experiments with iPro
verModulo show that proof search is indeed improved\, in par
ticular for set theories.
DTSTART;TZID=Europe/Paris:20151103T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201511031
100
UID:LSVsemLSV.201511031100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Complex Queries over Event Streams
STATUS:CONFIRMED
ATTENDEE;CN="Sylvain Hallé
":
MAILTO:no@spam.com
DESCRIPTION:
In this presentation\, we will discuss the problem of analyz
ing event logs\, i.e. any ordered sequence of data elements.
Two specific questions will be addressed. First\, how can w
e query an event log? This problem will lead us to talk abou
t the concept of Complex Event Processing\, which we can see
as a generalization of classical temporal logics. Secondly\
, how can we classify a set of logs into families\, and what
do these families represent intuitively? Preliminary result
s and an an implemetation of these concepts will also be dis
cussed.
DTSTART;TZID=Europe/Paris:20150929T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201509291
100
UID:LSVsemLSV.201509291100@lsv.ens-cachan.fr
LOCATION:Auditorium Daniel Chemla (Bât. Institut D'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Approximate counting in SMT and value estimation for probabi
listic programs
STATUS:CONFIRMED
ATTENDEE;CN="Dmitry Chistikov
":
MAILTO:no@spam.com
DESCRIPTION:
#SMT\, or model counting for logical theories\, is a well-kn
own hard problem that generalizes such tasks as counting the
number of satisfying assignments to a Boolean formula and c
omputing the volume of a polytope. In the realm of satisfiab
ility modulo theories (SMT) there is a growing need for mode
l counting solvers\, coming from several application domains
(quantitative information flow\, static analysis of probabi
listic programs). In this work\, we show a reduction from an
approximate version of #SMT to SMT. We focus on the theorie
s of integer arithmetic and linear real arithmetic. We propo
se model counting algorithms that provide approximate soluti
ons with formal bounds on the approximation error. They run
in polynomial time and make a polynomial number of queries t
o the SMT solver for the underlying theory\, exploiting ``fo
r free'' sophisticated heuristics implemented within modern
SMT solvers. We have implemented the algorithms and used the
m to solve a value estimation problem for a model of loop-fr
ee probabilistic programs with nondeterminism. Joint work wi
th Rayna Dimitrova and Rupak Majumdar.
DTSTART;TZID=Europe/Paris:20150602T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201506021
100
UID:LSVsemLSV.201506021100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Small universal Petri nets with inhibitor arcs
STATUS:CONFIRMED
ATTENDEE;CN="Serghei Verlan
":
MAILTO:no@spam.com
DESCRIPTION:
We investigate the problem of the construction of small-size
universal Petri nets with inhibitor arcs. We consider four
descriptional complexity parameters: the number of places\,
transitions\, inhibitor arcs\, and the maximal degree of a t
ransition. Each of these parameters is aimed to be minimized
\, a special attention being given to the number of places.
We give several constructions that highlight interesting tra
de-offs. Using equivalencies between models our results can
be translated to vector addition systems with zero check\, m
ultiset rewriting with forbidding conditions\, or to P syste
ms with inhibitors.
DTSTART;TZID=Europe/Paris:20150512T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201505121
100
UID:LSVsemLSV.201505121100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Reachability in Two-Dimensional Vector Addition Systems with
States is PSPACE-complete
STATUS:CONFIRMED
ATTENDEE;CN="Stefan Göller
":
MAILTO:no@spam.com
DESCRIPTION:
The reachability problem for vector addition systems with st
ates (VASS) is shown PSPACE-complete when the dimension is t
wo. This improves on a previously known doubly-exponential t
ime bound established by Howell\, Rosier\, Huynh and Yen in
1986. The coverability and boundedness problems are also not
ed to be PSPACE-complete. Some complexity results are also g
iven for the reachability problem in two-dimensional VASS an
d in integer VASS when numbers are encoded in unary.
DTSTART;TZID=Europe/Paris:20150414T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201504141
100
UID:LSVsemLSV.201504141100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Synthesis of Recursive Programs
STATUS:CONFIRMED
ATTENDEE;CN="Martin Lange
":
MAILTO:no@spam.com
DESCRIPTION:
Temporal logics are widely used in the specification and ver
ification of reactive and concurrent systems for the purpose
of building correct systems. Verification through model che
cking for instance is used to prove that a system\, construc
ted in a possibly faulty way\, satisfies a formal specificat
ion. Synthesis aims at eliminating errors in the constructio
n phase already: a system (model) should automatically be de
rived from the formal specification such that satisfaction i
s guaranteed. Synthesis is therefore closely related to a lo
gic's satisfiability problem: apart from deciding whether a
formula has a model\, such a model should also be returned.
In this talk we will present a generic game-theoretic approa
ch to the satisfiability problems for various temporal logic
s. Typical known logics that can be embedded into MSO have t
he finite model property though\, i.e. synthesis for these l
ogics is restricted to finite models only. In order to creat
e the theoretical foundations for synthesis of infinite-stat
e systems like recursive programs for instance it is necessa
ry to consider temporal logics beyond MSO that do not have t
he finite model property. There is only a narrow gap between
the finite model property on one side and undecidability on
the other. A family of temporal specification languages in
this corridor - therefore suitable for such synthesis purpos
es - is obtained by enriching classical temporal logics with
visibly pushdown languages.
DTSTART;TZID=Europe/Paris:20150324T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201503241
100
UID:LSVsemLSV.201503241100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Confluence of (non-terminating) layered rewrite systems by c
ritical pair analysis
STATUS:CONFIRMED
ATTENDEE;CN="Jean-Pierre Jouannaud
":
MAILTO:no@spam.com
DESCRIPTION:
Knuth and Bendix showed long ago that confluence of a termin
ating first-order rewrite system can be reduced to the joina
bility of its finitely many critical pairs. But there are no
n-terminating critical pair free rewrite systems which are n
on-confluent\, like R={f(x\,c(x)) -> a\, f(c(x)\,x) -> b\, g
-> c(g)}. We investigate here the case of layered systems f
or which a given lefthand side cannot be overlapped by other
lehthand sides unless at the root. We will also require tha
t the maximal number of redexes along a path from root to le
aves does not grow along reductions. R is a layered system.
Using novel unification techniques in infinite trees\, we sh
ow that layered systems are confluent provided their root cr
itical pairs\, in finite or infinite trees\, have decreasing
diagrams. We will also show that the redex-depth non-increa
sing condition is necessary. This work is part of a program
for designing new methods for showing confluence based on a
critical pair analysis when reductions are non-terminating (
as it is the case for type-theoretic raw terms\, because of
beta-reductions and elimination).
DTSTART;TZID=Europe/Paris:20150317T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201503171
100
UID:LSVsemLSV.201503171100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
A semantic study of higher-order model-checking
STATUS:CONFIRMED
ATTENDEE;CN="Charles Grellois
":
MAILTO:no@spam.com
DESCRIPTION:
Using higher-order recusion schemes\, one can model the comp
utation flow of functional programs\, and produce trees abst
racting their set of executions. The higher-order model-chec
king problem is concerned with the verification of a logical
property -- typically expressed in monadic second-order log
ic -- over this tree. A key feature of this logic being that
it allows to express finitary as well as infinitary propert
ies. Ong proved the decidability of this problem in 2006 usi
ng game semantics to analyze higher-order recursion. Since t
hen\, other semantic approaches lead to alternate proofs\, e
ach of them bringing a new semantic insight to the problem.
One of them\, by Kobayashi and Ong\, made use of intersectio
n types. In this talk\, I will introduce the higher-order mo
del-checking problem\, and explain how Paul-André Melliès an
d I could obtain a new proof of Ong's decidability result by
carefully analyzing the Kobayashi-Ong type system at the li
ght of linear logic and of its semantics.
DTSTART;TZID=Europe/Paris:20150303T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201503031
100
UID:LSVsemLSV.201503031100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Process Mining as Approximation and Verification Problems
STATUS:CONFIRMED
ATTENDEE;CN="Josep Carmona
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk I would present recent contributions mainly foc
used on discovery\, a very challenging problem in the area o
f process mining. Several theories like the theory of region
s\, numerical abstract domains and satisfiability will be us
ed to provide different algorithms to solve the discovery pr
oblem. Finally\, current challenges and directions will be p
resented to trigger the interest in the process mining field
.
DTSTART;TZID=Europe/Paris:20150120T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201501201
100
UID:LSVsemLSV.201501201100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Computability path ordering
STATUS:CONFIRMED
ATTENDEE;CN="Frédéric Blanqui
":
MAILTO:no@spam.com
DESCRIPTION:
We study here the computability path ordering (CPO)\, aiming
at carrying out termination proof for higher-order calculi.
CPO appears to be the ultimate improvement of the higher-or
der recursive path ordering (HORPO) in the sense that this d
efinition captures the essence of computability arguments à
la Tait and Girard\, therefore explaining the name of the im
proved ordering. We show that CPO allows to consider higher-
order rewrite rules in a simple type discipline with inducti
ve types\, that most of the guards present in the recursive
calls of its core definition cannot be relaxed in any natura
l way without loosing well-foundedness\, and that the preced
ence on function symbols cannot be made more liberal anymore
. (Joint work with J.-P. Jouannaud and A. Rubio.)
DTSTART;TZID=Europe/Paris:20150113T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201501131
100
UID:LSVsemLSV.201501131100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
L'enseignement de l'informatique
STATUS:CONFIRMED
ATTENDEE;CN="Serge Abiteboul
":
MAILTO:no@spam.com
DESCRIPTION:
Histoire rapide. Actualités. Analyse du problème : enseigner
pourquoi\, quoi\, à qui\, comment et par qui. On abordera s
i le temps le permet plus généralement l'inclusion numérique
et la littératie numérique.
DTSTART;TZID=Europe/Paris:20141216T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201412161
100
UID:LSVsemLSV.201412161100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Qualitative Analysis of Synchronizing Probabilistic Systems
STATUS:CONFIRMED
ATTENDEE;CN="Mahsa Shirmohammadi
":
MAILTO:no@spam.com
DESCRIPTION:
Markov decision processes (MDPs) are finite-state probabilis
tic systems with both strategic and random choices\, hence w
ell-established to model the interactions between a controll
er and its randomly responding environment. An MDP is viewed
as a 1/2-player stochastic game played in rounds when the c
ontroller chooses an action\, and the environment chooses a
successor according to a fixed probability distribution. Rec
ently\, MDPs have been viewed as generators of sequences of
probability distributions over states\, called the distribut
ion-outcome. We introduce synchronizing conditions defined o
n distribution-outcomes\, which intuitively requires that so
me (group of) state(s) tend to accumulate all the probabilit
y mass. We consider the following modes of synchronization:
the always mode where all distributions of the distribution-
outcome must be synchronized\, the eventually mode where som
e distributions must be synchronized\, the weakly mode where
infinitely many distributions must be synchronized\, and th
e strongly mode where all but finitely many distributions mu
st be synchronized. For each synchronizing mode\, we study t
hree winning modes: sure\, almost-sure and limit-sure. In th
is talk\, we present the various synchronization modes and w
inning modes\, as well as an overview of the key properties
for their analysis. We also give hints on synchronization in
probabilistic automata (PAs)\, that are kind of MDPs where
controllers are restricted to use only word-strategies; i.e.
no ability to observe the history of the system execution\,
but the number of choices made so far. This talk will be co
ncluded by introducing different variants of synchronization
for timed and weighted automata including synchronization t
o a unique location with possibly different clock valuation
or accumulated weight\, as well as synchronization with a sa
fety condition forbidding the automaton to visit states outs
ide a safety-set during synchronization (e.g. energy constra
ints). The talk is based on Mahsa Shirmohammadi's PhD thesis
\, which is carried out jointly in ULB (Belgium) and LSV\, E
NS Cachan (France). The official defense takes place in Brus
sels.
DTSTART;TZID=Europe/Paris:20141202T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201412021
100
UID:LSVsemLSV.201412021100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Aspects of dynamic complexity
STATUS:CONFIRMED
ATTENDEE;CN="Thomas Schwentick
":
MAILTO:no@spam.com
DESCRIPTION:
In most real-life databases data changes frequently and thus
makes efficient query answering challenging. Auxiliary data
might help to avoid computing query answers from scratch al
l the time. One way to study this incremental maintenance sc
enario is from the perspective of dynamic algorithms with
the goal to reduce (re-)computation time. Another option is
to investigate it from the perspective of low-level parallel
computational complexity [1] or parallelizable database que
ries [2]. As the "lowest" complexity class AC^0 (with a suit
able unifomity condition) and the core of the standard datab
ase query language SQL both coincide with first-order predic
ate logic\, one naturally arrives at the question which quer
ies can be answered/maintained dynamically with first-order
predicate logic (DynFO). The most intensely investigated que
ry in Dynamic Complexity is the reachability query on graphs
(arguably the "simplest recursive" query). It has been show
n that it can be maintained in DynFO on undirected [1] or ac
yclic directed graphs [2] and on directed embedded planar gr
aphs [3]. Recently it could be shown that it can be maintain
ed in DynFO\, for the class of all directed graphs. The talk
will give an introduction into dynamic complexity\, survey
some of its most important results\, and report about recent
work on fragments of DynFO. [1] Sushant Patnaik and Neil I
mmerman. Dyn-FO: A parallel\, dynamic complexity class. J. C
omput. Syst. Sci.\, 55(2):199--209\, 1997. [2] Guozhu Dong a
nd Jianwen Su. Incremental and decremental evaluation of tra
nsitive closure by first-order queries. Inf. Comput.\, 120(1
):101--106\, 1995. [3] Samir Datta\, William Hesse and Ragha
v Kulkarni. Dynamic Complexity of Directed Reachability and
Other Problems. ICALP 2014.
DTSTART;TZID=Europe/Paris:20141118T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201411181
100
UID:LSVsemLSV.201411181100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
The CVC4 SMT Solver
STATUS:CONFIRMED
ATTENDEE;CN="Morgan Deters
":
MAILTO:no@spam.com
DESCRIPTION:
Satisfiability Modulo Theories (SMT) solvers leverage resear
ch advances in SAT solving and decision procedures to solve
Boolean combinations of constraints written in an expressive
language combining different background theories. CVC4 is a
solver for these SMT problems with a number of features use
ful in verification\, static analysis\, synthesis\, symbolic
execution\, and other domains. This talk provides an overvi
ew of SMT and describes the main features of SMT solvers\, w
ith a focus on CVC4. I discuss various aspects of CVC4's int
ernals\, including its architecture\, its capacity for deali
ng with quantifiers\, its finite model finder\, and the line
ar arithmetic solver. CVC4\, jointly developed at New York U
niversity and the University of Iowa\, is freely available f
or both research and commercial use under an open-source lic
ense.
DTSTART;TZID=Europe/Paris:20141104T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201411041
100
UID:LSVsemLSV.201411041100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Effectively regular downward closures
STATUS:CONFIRMED
ATTENDEE;CN="Georg Zetzsche
":
MAILTO:no@spam.com
DESCRIPTION:
The downward closure of a language is the set of all (not ne
cessarily contiguous) subwords of its members. It is a well-
known consequence of Higman's Lemma that the downward closur
e of every language is regular. Aside from encoding interest
ing counting properties\, the downward closure constitutes a
promising abstraction: If L is the set of action sequences
of a system\, then the downward closure of L is precisely wh
at is observed through a lossy channel\, i.e. when actions c
an go unnoticed arbitrarily. Hence\, if the downward closure
is available as a regular language\, the equivalence and ev
en inclusion of system behaviors can be decided with respect
to such observations. However\, there are only few classes
of languages for which it is known how to compute the downwa
rd closure of a given language as a finite automaton. This t
alk presents new approaches to this problem.
DTSTART;TZID=Europe/Paris:20141028T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201410281
100
UID:LSVsemLSV.201410281100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Abstract approach and verification in high-performance compu
ting
STATUS:CONFIRMED
ATTENDEE;CN="Stanislav Böhm
":
MAILTO:no@spam.com
DESCRIPTION:
The goal of the talk is to introduce a tool for simplifying
development of applications in the area of scientific and en
gineering computations for distributed memory systems. Our g
oal is to provide a rapid prototyping environment\, automati
cally generate efficient programs and verify their performan
ce\, scalability\, and correctness. A unifying element in th
e approach is a visual programming language inspired by Colo
red Petri Nets. The second part of the talk will provide an
overview about verification tools in the area of Message Pas
sing Interface (MPI). MPI is a standard programming interfac
e in today's supercomputers and even there are lots of suppo
rting tools for MPI\, there are only few verification tools.
DTSTART;TZID=Europe/Paris:20141021T140000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201410211
400
UID:LSVsemLSV.201410211400@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Well-structured pushdown systems
STATUS:CONFIRMED
ATTENDEE;CN="Mizuhito Ogawa
":
MAILTO:no@spam.com
DESCRIPTION:
Well-structured pushdown systems (WSPDS) is an extension of
Well-structured transition systems (WSTS) with a single stac
k. We investigate decidability of coverability of WSPDS. Var
ious VASS extensions (RVASS\, BVAS\, VASS with one-zero test
) are examples of the forward technique\, and Dense timed pu
shdown automata and Nested Timed Automata are those of the b
ackward technique. We also discuss on related work including
another recent WSPDS result by Jerome Leroux.
DTSTART;TZID=Europe/Paris:20141014T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201410141
100
UID:LSVsemLSV.201410141100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Model Theory of XPath with data tests
STATUS:CONFIRMED
ATTENDEE;CN="Santiago Figueira
":
MAILTO:no@spam.com
DESCRIPTION:
We develop the basic model theory of XPath with data (in)equ
ality tests over the class of data trees\, i.e.\, the class
of trees where each node contains a label from a finite alph
abet and a data value from an infinite domain. We provide no
tions of bisimulations (both general and bounded) for XPath
logics containing only 'child'\, or both 'child' and 'parent
' navigational axes. We show that these notions precisely ca
pture the logical equivalence relation associated with each
fragment\, and show two results where the tool of bisimulati
on plays a central role: characterization and definability.
The former says that certain logic is the bisimulation-invar
iant fragment of first order; the latter gives necessary and
sufficient conditions for a class of pointed data trees to
be definable by a set of formulas or by a single formula.
DTSTART;TZID=Europe/Paris:20140930T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201409301
100
UID:LSVsemLSV.201409301100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Engineering and University Relations
STATUS:CONFIRMED
ATTENDEE;CN="Michel Bénard and Vincent Simonet
":
MAILTO:no@spam.com
DESCRIPTION:
Google Engineering et en particulier le centre de Paris sero
nt d'abord présentés. Ensuite les objectifs et les mécanisme
s de collaboration avec les universités et centres de recher
che. La présentation sera suivie d'une session de questions
et réponses. Slides de la présentation.
DTSTART;TZID=Europe/Paris:20140923T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201409231
100
UID:LSVsemLSV.201409231100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Computation in sets with atoms
STATUS:CONFIRMED
ATTENDEE;CN="Sławomir Lasota
":
MAILTO:no@spam.com
DESCRIPTION:
In sets with atoms\, finiteness is relaxed to ''finiteness u
p to permutation''\, formally defined as orbit-finiteness. T
he talk will be an overview of models of computation\, such
as (various kinds of) automata\, Petri nets or Turing machin
es\, where state spaces\, input alphabets and transition rel
ations are orbit-finite sets with atoms. I will focus on fun
damental properties\, such as (lack of) determinisation\, an
d on fundamental analysis problems\, such as reachability. I
will also mention recently discovered links to descriptive
complexity\, constraint satisfaction\, and model theory.(joi
nt work with Mikołaj Bojańczyk\, Bartek Klin\, Joanna Ochrem
iak and Szymon Toruńczyk)
DTSTART;TZID=Europe/Paris:20140708T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201407081
100
UID:LSVsemLSV.201407081100@lsv.ens-cachan.fr
LOCATION:AmphithÃ©Ã¢tre 121 (BÃ¢t. De Vinci)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Towards synthesis and verification for articulated robots ?
STATUS:CONFIRMED
ATTENDEE;CN="Nicolas Perrin
":
MAILTO:no@spam.com
DESCRIPTION:
Over the last ten years\, hybrid system theory has been incr
easingly used in the field of robotics\, where the need for
verification is often high\, especially in contexts where ro
bots interact with humans. However\, up to now\, most succes
sful results were obtained with robots that can be considere
d as points\, such as mobile robots\, networks of unmanned v
ehicles\, etc. Articulated robots (which are ubiquitous in s
ome industries) present a different challenge due to their d
ynamical and geometrical complexity. The classical control f
ramework for such robots can realize complex tasks with simp
le specifications\, but it relies on numerical methods that
leave a lot of uncertainty on the motions actually produced.
I will introduce this framework and explain some of the spe
cific issues associated with it. Then\, I will present a few
problems that examplify the type of difficulty that must be
overcome to enable relevant synthesis and verification for
articulated robots.
DTSTART;TZID=Europe/Paris:20140701T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201407011
100
UID:LSVsemLSV.201407011100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Dependence and Independence in Logic
STATUS:CONFIRMED
ATTENDEE;CN="Erich Grädel
":
MAILTO:no@spam.com
DESCRIPTION:
There have been a number of proposals for incorporating the
concepts of dependence or independence into mathematical log
ic. Classical variants include Henkin quantifiers and indepe
ndence friendly logics; a more modern approach\, triggered b
y Väänänen's dependence logic\, treats notions of dependence
and independence as atomic properties and not as annotation
s of quantifiers\, and has motivated the construction and an
alysis of a large variety of logics based on different notio
ns of dependence and independence\, many of which have close
connections to dependency concepts from database theory. Th
e key difference to classical logical formalisms is that dep
endence and independence manifest themselves not for a singl
e assignment\, mapping variables to elements of a structure\
, but only for a set of such assignments. Accordingly\, mode
l-theoretic semantics for logics of dependence and independe
nce refer to structures together with a set of assignments (
called a team) and thus differ substantially from the Tarski
-style semantics of first-order logic\, second-order logic a
nd similar formalisms. We shall describe different logics of
dependence and independence and examine their expressive po
wer. We design model-checking games for logics with team sem
antics in a general and systematic way. The second-order fea
tures of team semantics are reflected by the notion of a con
sistent winning strategy which is also a second-order notion
in the sense that it depends not on single plays but on the
space of all plays that are compatible with the strategy. B
eyond the application to logics with team semantics\, we iso
late an abstract\, purely combinatorial definition of such g
ames\, which may be viewed as second-order reachability game
s\, and study their algorithmic properties. A number of exam
ples are provided that show how logics with team semantics e
xpress familiar combinatorial problems in a somewhat unexpec
ted way. Based on our games\, we provide a complexity analys
is of logics with teams semantics. We shall also discuss the
recently discovered connections between logics with team se
mantics and fixed-point logics\, and analyze these connectio
ns in game-theoretic terms.
DTSTART;TZID=Europe/Paris:20140610T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201406101
100
UID:LSVsemLSV.201406101100@lsv.ens-cachan.fr
LOCATION:Auditorium Daniel Chemla (Bât. Institut D'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Asymptotic behaviour of max-plus and min-plus automata
STATUS:CONFIRMED
ATTENDEE;CN="Laure Daviaud
":
MAILTO:no@spam.com
DESCRIPTION:
Min-plus and max-plus automata are non deterministic finite
automata with weights (non-negative integers) on transitions
. These automata compute functions from the set of words to
the set of non negative integers including an infinite value
. Questions such as equivalence or comparison are undecidabl
e problems. This implies the impossibility to precisely desc
ribe the evolution of these functions. In this talk\, I will
give results about the description of the asymptotic behavi
our of these functions. More precisely\, given a function f
computed by a min-plus (resp. max-plus) automaton\, we consi
der a function from the set of positive integers defined by
g:n -> max{f(w) | |w| < n} (resp. g:n -> min{f(w) | |w|>n}.
I will present two results about the description of g. First
\, the asymptotic behaviour of g is of the form n^a where a
is a rationnal from [0\,1]. Second\, it is possible to appro
ximate the ratio g(n)/n. These questions are related with th
e approximation of sets of matrices over the tropical (resp.
max-plus) semiring. This talk is based on joint works with
Thomas Colcombet and Florian Zuleger.
DTSTART;TZID=Europe/Paris:20140513T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201405131
100
UID:LSVsemLSV.201405131100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Quantitative evaluation of non-Markovian models through the
approach of stochastic state classes: applications and futur
e issues
STATUS:CONFIRMED
ATTENDEE;CN="Laura Carnevali
":
MAILTO:no@spam.com
DESCRIPTION:
The method of stochastic state classes supports steady state
and transient analysis of models that encompass multiple ti
mers with general distribution and possibly bounded support.
When the model underlies a Markov Regenerative Process (MRP
) that always reaches a regeneration point within a finite n
umber of steps\, transient analysis can be limited to the fi
rst regeneration epoch and repeated from every regenerative
point. This supports efficient derivation of the local and g
lobal kernels that characterize the MRP behavior and enables
transient evaluation through the numerical integration of g
eneralized Markov renewal equations. Applications of the app
roach through the Oris Tool are illustrated referring to the
evaluation of availability measures for maintenance procedu
res. Future research directions are discussed in the area of
probabilistic schedulability analysis of real-time systems.
DTSTART;TZID=Europe/Paris:20140415T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201404151
100
UID:LSVsemLSV.201404151100@lsv.ens-cachan.fr
LOCATION:Auditorium Daniel Chemla (Bât. Institut D'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Paraconsistency and Team Semantics
STATUS:CONFIRMED
ATTENDEE;CN="Pietro Galliani
":
MAILTO:no@spam.com
DESCRIPTION:
Team Semantics is a generalization of Tarski's semantics for
first-order logic which defines satisfiability with respect
to sets of assignments\, rather than with respect to single
assignments. In recent years\, this semantics has emerged a
s a very general formalism for the study of dependence notio
ns and their relations; and\, furthermore\, this semantics h
as lately proved to be of interest for the purposes of belie
f representation and belief updating. In this talk\, I will
discuss a simple variation in the definition of team semanti
cs (corresponding\, from the perspective of game-theoretic s
emantics\, to reasoning in terms of non-losing strategies ra
ther than winning strategies)\, and its consequences\, and i
ts possible applications.
DTSTART;TZID=Europe/Paris:20140318T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201403181
100
UID:LSVsemLSV.201403181100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Equivalence checking of stack-based infinite-state systems
STATUS:CONFIRMED
ATTENDEE;CN="Stefan Göller
":
MAILTO:no@spam.com
DESCRIPTION:
I will give a survey of some results concerning the computat
ional complexity of language equivalence and bisimulation eq
uivalence of stack-based infinite-state systems like higher-
order pushdown automata\, pushdown automata and deterministi
c one-counter automata.In particular I will try to convey th
e proof ideas to the following results: (i) bisimilarity of
order-two pushdown automata is undecidable\, (ii) bisimilari
ty of pushdown automata is non-elementary and (iii) equivale
nce of deterministic one-counter automata is NL-complete. If
there is sufficient time left I will mention some concrete
problems that I think are worth investigating for possibly o
btaining a better understanding of equivalence checking of s
tack-based infinite-state systems.
DTSTART;TZID=Europe/Paris:20140311T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201403111
100
UID:LSVsemLSV.201403111100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Synthesis of Tissue Systems
STATUS:CONFIRMED
ATTENDEE;CN="Maciej Koutny
":
MAILTO:no@spam.com
DESCRIPTION:
Tissue systems are a computational abstraction of the chemic
al reactions and transport of molecules in a tissue. The tal
k will consider the problem of synthesising tissue systems f
rom specifications of observed or desired behaviour given in
the form of transition systems. The talk will show how a Pe
tri net solution to this problem\, based on the notion of re
gions\, yields a method for automated synthesis of tissue sy
stems from transition systems. It will be first assumed that
the input of the algorithm contains information about the t
opology of the system to be constructed\, and then the case
when such a topology is not known in advance and has yet to
be determined will be discussed.
DTSTART;TZID=Europe/Paris:20140304T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201403041
100
UID:LSVsemLSV.201403041100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Interval methods for proving properties of dynamical systems
; application to the validation of the control lows for the
sailboat robot VAIMOS.
STATUS:CONFIRMED
ATTENDEE;CN="Luc Jaulin
":
MAILTO:no@spam.com
DESCRIPTION:
This talk presents an original method combining interval ana
lysis and Lyapunov theory for stability analysis of uncertai
n dynamical systems. The principle of the approach is to rep
resent uncertain systems by differential inclusions and then
to perform a Lyapunov analysis in order to cast the stabili
ty problem within a set-inversion framework. With this appro
ach\, we can show that for all feasible perturbations\, (i)
there exists a safe subset A of the state space the system c
annot escape as soon as it enters in it and (ii) if the syst
em is outside A\, it cannot stay outside A forever. In a sec
ond step\, the methodology is used to build reliable robust
controllers. An illustration related to the line following p
roblem of sailboat robots is then provided. After introducin
g the basic notions on interval analysis and Lyapunov theory
\, I will show how these tools can be used for stability ana
lysis of nonlinear systems. Then an experimental validation
that took place on January 2012 will then be presented. On t
his experiment\, the autonomous sailboat robot Vaimos\, has
gone from Brest to Douarnenez (more than 100 km). More detai
ls can be found at http://www.ensta-bretagne.fr/jaulin/vaimo
sdouarn.html. This talk will be presented in a pedagogical w
ay in order to be easily understood by non specialists.
DTSTART;TZID=Europe/Paris:20140218T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201402181
100
UID:LSVsemLSV.201402181100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Verification of Imperative Programs by Constraint Logic Prog
ram Transformation
STATUS:CONFIRMED
ATTENDEE;CN="Alberto Pettorossi
":
MAILTO:no@spam.com
DESCRIPTION:
We present a method for verifying partial correctness proper
ties of imperative programs that manipulate integers and arr
ays by using techniques based on the transformation of const
raint logic programs (CLP). We use CLP as a metalanguage for
representing (i) imperative programs\, (ii) their operation
al semantics\, and (iii) their properties. Our method incorp
orates into the field of program verification many technique
s which have been developed during the last years in the fie
ld of program transformation. We have implemented our method
in a verification system. That system\, called VeriMAP\, is
competitive with respect to state-of-the-art tools for prog
ram verification.
DTSTART;TZID=Europe/Paris:20140212T103000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201402121
030
UID:LSVsemLSV.201402121030@lsv.ens-cachan.fr
LOCATION:Auditorium Daniel Chemla (Bât. Institut D'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Proving Theorems by Program Transformation
STATUS:CONFIRMED
ATTENDEE;CN="Maurizio Proietti
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk I will present an overview of the unfold/fold p
roof method\, a method for proving theorems about programs b
ased on program transformation. As a metalanguage for specif
ying programs and program properties we adopt constraint log
ic programming (CLP) and we consider a set of transformation
rules (including the familiar unfolding and folding rules)
that preserve the semantics of CLP programs. Then\, we show
how program transformation strategies can be used\, similarl
y to theorem proving tactics\, for guiding the application o
f the transformation rules and inferring the properties to b
e proved. We work out three examples: (i) the proof of predi
cate equivalences\, applied to the verification of equality
between CCS processes\, (ii) the proof of first order formul
as via an extension of the quantifier elimination method\, a
nd (iii) the proof of temporal properties of infinite state
concurrent systems\, by using a transformation strategy that
performs program specialization.
DTSTART;TZID=Europe/Paris:20140211T140000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201402111
400
UID:LSVsemLSV.201402111400@lsv.ens-cachan.fr
LOCATION:Auditorium Daniel Chemla (Bât. Institut D'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Are formal methods the future of air traffic control ? (Is t
here an autopilot on board ?)
STATUS:CONFIRMED
ATTENDEE;CN="Gilles Dowek
":
MAILTO:no@spam.com
DESCRIPTION:
Decentralized air traffic control is a concept of operation
s where air traffic control is decentralized to aircrafts an
d on board computers are used to assist and/or replace the p
ilots in deciding the route of the aircraft. In some experim
ental concepts\, the full operation of the aircraft is deleg
ated to on board computers. Such concepts can be accepted by
the general population only if the computer systems used ar
e extremely safe and this makes air traffic control a major
domain of application for formal methods. The diversity prob
lems in air traffic control leads to favor no particular typ
e of formal methods but to use them all as different methods
address different types of problems.
DTSTART;TZID=Europe/Paris:20140204T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201402041
100
UID:LSVsemLSV.201402041100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
A formalization of bisimulation-up-to techniques and their m
eta-theory
STATUS:CONFIRMED
ATTENDEE;CN="Matteo Cimini
":
MAILTO:no@spam.com
DESCRIPTION:
Bisimilarity of two processes is formally established by pro
ducing a bisimulation relation\, i.e. a set of pairs of proc
ess expressions that contains those two processes and obeys
certain closure properties. In many situations\, particularl
y when the underlying labeled transition system is unbounded
\, these bisimulation relations can be large and even infini
te. The bisimulation-up-to technique has been developed to r
educe the size of the relations to exhibit while retaining s
oundness\, that is\, the guarantee of the existence of a bis
imulation. Such techniques make defining candidate relations
easier and they significantly reduce the amount of work in
proofs. Furthermore\, they are increasingly becoming a cruci
al ingredient in the automated checking of bisimilarity. In
this talk\, we present our experience in using the Abella th
eorem prover for the formalization of the meta theory of sev
eral major bisimulation-up-to techniques for the process cal
culi CCS and the pi-calculus. Our formalization is based on
recent work on the proof theory of least and greatest fixpoi
nts for accommodating the heavy use of coinductively defined
relations and coinductive proofs about such relations. An i
mportant feature of our formalization is that our definition
s and proofs are\, in most cases\, straightforward translati
ons of published informal definitions\, and our proofs clari
fy several technical details of the informal descriptions. T
he presence of binders\, as in the pi-calculus\, is notoriou
sly a delicate aspect to treat in formal proofs but we show
that the underlying proof theoretic foundations of Abella ma
kes it possible to smoothly lift the results from CCS to the
pi-calculus. This is thanks to the use of lambda-tree synta
x and generic reasoning through the nabla quantifier.
DTSTART;TZID=Europe/Paris:20140121T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201401211
100
UID:LSVsemLSV.201401211100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Infinite sequential Nash equilibrium
STATUS:CONFIRMED
ATTENDEE;CN="Stéphane Le Roux
":
MAILTO:no@spam.com
DESCRIPTION:
In game theory\, the concept of Nash equilibrium reflects th
e collective stability of some individual strategies chosen
by selfish agents. The concept pertains to different classes
of games\, e.g. the sequential games\, where the agents pla
y in turn. Two existing results are relevant here: first\, a
ll finite such games have a Nash equilibrium (w.r.t. some gi
ven preferences) iff all the given preferences are acyclic;
second\, all infinite such games have a Nash equilibrium\, i
f they involve two agents who compete for victory and if the
actual plays making a given agent win (and the opponent los
e) form a quasi-Borel set. This talk generalises these two r
esults via a single result. More generally\, under the axiom
atic of Zermelo-Fraenkel plus the axiom of dependent choice
(ZF+DC)\, it proves a transfer theorem for infinite sequenti
al games: if all two-agent win-lose games that are built usi
ng a well-behaved class of sets have a Nash equilibrium\, th
en all multi-agent multi-outcome games that are built using
the same well-behaved class of sets have a Nash equilibrium\
, provided that the inverse relations of the agents' prefere
nces are strictly well-founded.
DTSTART;TZID=Europe/Paris:20140107T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201401071
100
UID:LSVsemLSV.201401071100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
A survey on regular cost-functions and their applications
STATUS:CONFIRMED
ATTENDEE;CN="Thomas Colcombet
":
MAILTO:no@spam.com
DESCRIPTION:
This talk will be the occasion to give an introduction to re
gular cost-functions\, to describe the main concepts involve
d\, to give an overview of the known results and open proble
ms\, and to show some applications. The theory of regular co
st-functions offer a quantitative extension to the notion of
regular language. Regular cost-functions can count\, for in
stance the number of occurrence of some patterns\, and can o
ptimize quantities (for instance compute nested infima and s
uprema). In particular\, some notions of resource consumptio
n can be easily expressed using regular cost-functions. Regu
lar cost-functions can be used over words\, finite of infini
te\, or trees\, finite or infinite (though infinite trees ar
e only partially understood so far). As it is the case for r
egular languages\, this theory comes with several decision p
rocedures and many forms of effectively equivalent computati
onal models such as automata (B-automata and S-automata)\, a
lgebra (stabilisation monoids)\, expressions (B-expressions
and S-expressions)\, or logics (cost-monadic second-order lo
gic). These results strictly extend their classical language
counterparts. The theory of regular cost-functions continue
s and uses the techniques and results developed formerly by
Hashiguchi\, Leung\, Simon and Kirsten since the early eight
ies. At the same it provides a uniform and more general fram
ework for understanding all these works. The central questio
n addressed by regular cost-functions is the ability to deci
de the existence of a bound on the range of some finitely re
presented function. On the one hand\, only concentrating on
bounds may be seen as a severe restriction (but otherwise\,
decidability would be immediately lost). On the other hand\,
many problems in computer science\, or in mathematics turn
out to be reducible to questions of existence of bounds on s
ome quantities. For this reason\, several non-trivial proble
ms can be shown decidable by reduction to cost-function deci
sion procedures. Let us cite for instance the finite power p
roperty (given a regular language L\, does there exist n suc
h that L^n=L*)\, the star height problem (given a regular la
nguage L and an integer k\, is it possible to write L as a r
egular expression using at most k nesting of Kleene stars) a
nd its extension to trees\, the finite substitution problem\
, the problem of finitely unfolding fixpoints of MSO formula
e while preserving their semantics\, some quantitative varia
nts of the Church synthesis problem\, or the decidability of
the Rabin-Mostowski hierarchy (a problem only partially sol
ved so far).
DTSTART;TZID=Europe/Paris:20131203T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201312031
100
UID:LSVsemLSV.201312031100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Meet Your Expectations With Guarantees: Beyond Worst-Case Sy
nthesis in Quantitative Games
STATUS:CONFIRMED
ATTENDEE;CN="Mickael Randour
":
MAILTO:no@spam.com
DESCRIPTION:
We extend the quantitative synthesis framework by going beyo
nd the worst-case. On the one hand\, classical analysis of t
wo-player games involves an adversary (modeling the environm
ent of the system) which is purely antagonistic and asks for
strict guarantees. On the other hand\, stochastic models li
ke Markov decision processes represent situations where the
system is faced to a purely randomized environment: the aim
is then to optimize the expected payoff\, with no guarantee
on individual outcomes. We introduce the beyond worst-case s
ynthesis problem\, which is to construct strategies that gua
rantee some quantitative requirement in the worst-case while
providing an higher expected value against a particular sto
chastic model of the environment given as input. This proble
m is relevant to produce system controllers that provide nic
e expected performance in the everyday situation while ensur
ing a strict (but relaxed) performance threshold even in the
event of very bad (while unlikely) circumstances. We study
the beyond worst-case synthesis problem for two important qu
antitative settings: the mean-payoff and the shortest path.
In both cases\, we show how to decide the existence of finit
e-memory strategies satisfying the problem and how to synthe
size one if one exists. We establish algorithms and we study
complexity bounds and memory requirements.
DTSTART;TZID=Europe/Paris:20131126T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201311261
100
UID:LSVsemLSV.201311261100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Structural tractability of counting solutions to conjunctive
queries
STATUS:CONFIRMED
ATTENDEE;CN="Stefan Mengel
":
MAILTO:no@spam.com
DESCRIPTION:
Conjunctive queries are a basic class of database queries eq
uivalent to select-project-join queries and strongly related
to constraint satisfaction problems. Most research on conju
nctive queries has focused on the so-called boolean conjunct
ive query problem\, short CQ\, which is\, given a query and
a database\, to decide if the query has any answers with res
pect to the database. While CQ is hard in general\, many 'is
lands of tractability' have been found based on the hypergra
phs associated to queries. Recently\, Pichler and Skritek ha
ve shown that these hypergraph based techniques are not suff
icient to guarantee tractability for the associated counting
problem #CQ\, i.e.\, given a conjunctive query and a databa
se\, determine the number of answers to the query. I will gi
ve a short introduction into conjunctive queries and present
joint work with Arnaud Durand in which we characterized exa
ctly the tractability frontier for #CQ for well-known hyperg
raph based classes of conjunctive queries.
DTSTART;TZID=Europe/Paris:20131112T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201311121
100
UID:LSVsemLSV.201311121100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
The Theory of Visibly Multistack Pushdown Systems
STATUS:CONFIRMED
ATTENDEE;CN="Salvatore La Torre
":
MAILTO:no@spam.com
DESCRIPTION:
Multi-stack pushdown systems (MPS) are a natural model of th
e control flow of multi-threaded programs. The intuition of
exploring computations up to a bounded number of context swi
tches has stimulated a series of interesting results in prog
ram verification\, such as for example the possibility of se
quentializing concurrent programs without maintaining the cr
oss-product of the involved threads\, and the study of the f
ormal theory of decidable subclasses. In this talk\, we focu
s on the formal languages theory of the classes of MPS with
the bounded-context switching\, scope-bounded\, phase-bounde
d\, and stack-ordered restrictions.
DTSTART;TZID=Europe/Paris:20131105T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201311051
100
UID:LSVsemLSV.201311051100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
BioModel Engineering - a Petri Net Perspective
STATUS:CONFIRMED
ATTENDEE;CN="Monika Heiner
":
MAILTO:no@spam.com
DESCRIPTION:
The talk describes a Petri net-based framework to model and
analyse biochemical networks\, such as gene regulatory\, sig
nal transduction or metabolic networks. The framework compri
ses the qualitative\, stochastic\, and continuous modelling
paradigms. Each perspective adds its contribution to the bet
ter understanding of the biochemical system under study. Thi
s will be illustrated by two examples showing how structural
analysis techniques\, specifically Petri net T-invariants\,
may be of help. First\, a technique is discussed supporting
modularisation and hierarchical representation of a given n
etwork by network coarsening. Second\, a case study is prese
nted where structural analysis helps to identify the core ne
twork and fragile nodes of a continuous network in the stead
y-state interpretation.
DTSTART;TZID=Europe/Paris:20131001T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201310011
100
UID:LSVsemLSV.201310011100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Updatable Strategy Logic
STATUS:CONFIRMED
ATTENDEE;CN="Christophe Chareton
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk\, we present a temporal multi-agent logic calle
d Updatable Strategy Logic (USL) which subsumes the main pro
positions in this area\, such as ATL-ATL*\, ATLsc and SL. Th
ese logics allow to express the capabilities of agents to en
sure the satisfaction of temporal properties. USL mainly dif
fers from SL in two ways. Semantically\, the notion of strat
egy composition is extended to enable an agent to refine her
strategy\, that is to update it without revoking it. Syntac
tically\, a new operator\, called "unbinder"\, is introduced
: it allows an agent to explicitly revoke a strategy\, where
as revocation is implicit in SL. USL allows to express new p
roperties of interactions between coalitions of agents. It a
lso allows to introduce a notion of "sustainability" for the
capabilities of agents to achieve objectives\, a sustainabl
e capability for an agent being a capability that still hold
s even after it has been employed. This makes USL strictly m
ore expressive than SL.
DTSTART;TZID=Europe/Paris:20130924T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201309241
100
UID:LSVsemLSV.201309241100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Synchronization Invariants
STATUS:CONFIRMED
ATTENDEE;CN="Klaus Draeger
":
MAILTO:no@spam.com
DESCRIPTION:
Invariants are an important tool for the verification of com
plex systems. One very simple class of invariants for compos
itional reasoning is given by linear constraints on the occu
rrences of synchronization sequences. This class of invarian
ts exhibits some quite interesting properties\, including co
nnections to mathematical fields such as topology. I am curr
ently investigating generalizations of these concepts to mor
e general structures than words\, and more general kinds of
systems\, such as probabilistic ones. In this talk\, I will
give an overview of this work in progress.
DTSTART;TZID=Europe/Paris:20130702T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201307021
100
UID:LSVsemLSV.201307021100@lsv.ens-cachan.fr
LOCATION:Amphithéâtre Tocqueville
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Contraint Satisfaction Problems and Algebra: a survey of rec
ent developments
STATUS:CONFIRMED
ATTENDEE;CN="Benoit Larose
":
MAILTO:no@spam.com
DESCRIPTION:
In the last 15 years\, universal algebraic techniques have l
ed to deep insights into the nature of the computational and
descriptive complexity of constraint satisfaction problems.
We present an overview of these techniques\, as well as res
ults and open questions in this area.
DTSTART;TZID=Europe/Paris:20130611T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201306111
100
UID:LSVsemLSV.201306111100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Deterministically Communicating MDPs
STATUS:CONFIRMED
ATTENDEE;CN="Madhavan Mukund
":
MAILTO:no@spam.com
DESCRIPTION:
The formal verification of large probabilistic models remain
s a challenge. To better exploit the concurrency that is oft
en present\, we introduce deterministically communicating Ma
rkov Decision Processes (DMDPs) in which the components sync
hronize to determine the local probability distribution for
their next moves. Two simultaneously enabled synchronization
s are guaranteed to involve disjoint sets of MDPs. As a resu
lt\, one can define the global behavior of a DMDP as a Marko
v chain without having to introduce schedulers. In order to
cope with the exponential size of this Markov chain in the n
umber of components\, we define an interleaved semantics in
terms of the local synchronization actions. The network stru
cture induces an independence relation on these actions. Usi
ng Mazurkiewicz trace theory\, we establish a strong relatio
nship between the interleaved semantics and the global Marko
v chain semantics. This allows us to construct a natural pro
bability measure with respect to the interleaved semantics.
Consequently\, verification of DMDPs can often be efficientl
y carried out using the interleaved semantics without having
to construct the global Markov chain. To illustrate this we
develop a statistical model checking (SMC) procedure under
the interleaved semantics and use it to verify a probabilist
ic algorithm for leader election over an anonymous ring. Our
method can easily cope with a ring containing 50 processes
while the same SMC procedure applied to the global Markov ch
ain (using PRISM) can only deal with rings containing at mos
t 3 processes. This is joint work with Sumit Kumar Jha\, Rat
ul Saha and P.S. Thiagarajan.
DTSTART;TZID=Europe/Paris:20130528T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201305281
100
UID:LSVsemLSV.201305281100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Parikh automata
STATUS:CONFIRMED
ATTENDEE;CN="Pierre McKenzie
":
MAILTO:no@spam.com
DESCRIPTION:
The Parikh automaton defined by Klaedtke and Ruess in 2003 a
mounts to a nondeterministic finite automaton equipped with
registers tallying up the number of occurrences of each tran
sition along a run. The final tally must belong to a prescri
bed semilinear set for an input word to be accepted. We will
discuss the expressivity and decidability properties of thi
s model and of extensions such as an affine variant\, in whi
ch transitions can induce affine transformations on the regi
sters\, and an unambiguous variant\, in which the automaton
is unambiguous. We will sketch their algebraic characterisat
ions and give bounds on the complexities of their languages.
This work is drawn from the recent PhD thesis of Michaël Cad
ilhac (Montréal) and is joint with Alain Finkel and Andreas
Krebs (Tübingen).
DTSTART;TZID=Europe/Paris:20130514T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201305141
100
UID:LSVsemLSV.201305141100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Programs\, domains\, and logic
STATUS:CONFIRMED
ATTENDEE;CN="Achim Jung
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk I will give an overview of some research questi
ons that over the years have inspired me and to which I have
contributed. While somewhat tutorial in nature\, I will als
o try to explain some of the more technical difficulties whi
ch we have encountered along the way\, and which have made m
e change direction a few times. We will begin with Scott's w
ork of the late 1960's\, when he began to lay the foundation
s for a "mathematical theory of computation"\, and the corre
spondence between programs and semantic models initiated by
Plotkin in 1977. I will explain the notion of a Scott domain
and its associated concepts of "finite element" and "approx
imation". We'll then see how the desire to deal with real nu
mbers and probabilities led to an interest in continuous dom
ains. Again we'll see its successes but also some of the pro
blems that appeared. For reasons of the latter\, the focus f
or me shifted towards topological spaces. Domain-style appro
ximation being no longer available\, this move entailed a cl
oser study of Stone dualities\, where instead of spaces one
considers "propositions" about elements of a space. Although
this may appear as a technical necessity\, it does actually
emphasise the link between semantics and program logics\, s
omething that Samson Abramsky advocated more than 20 years a
go in his "Domain theory in logical form".
DTSTART;TZID=Europe/Paris:20130409T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201304091
100
UID:LSVsemLSV.201304091100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
The theory of regular cost functions\, from finite words to
infinite trees.
STATUS:CONFIRMED
ATTENDEE;CN="Denis Kuperberg
":
MAILTO:no@spam.com
DESCRIPTION:
The theory of regular cost functions\, initiated by Colcombe
t and following work with Mikołaj Bojańczyk\, is a satisfyin
g framework to extend a large spectrum of results on regular
languages to a quantitative setting. I will present the the
ory\, and give an overview of results obtained in my thesis.
On finite and infinite words\, we generalize a number of re
sults from the theory of regular languages\, often by showin
g equivalence between different formalisms (in terms of auto
mata\, logics\, or semigroups). In particular we show that w
e can extend the notion of syntactic congruence to this quan
titative framework. We also study the temporal class\, which
does not have a counterpart in language theory. On infinite
trees\, we show that the Rabin-Kupferman-Vardi theorem on l
anguages is generalized in an unexpected way\, and gives ris
e to the class of quasi-weak cost functions. The study of th
is class allows us to obtain a decidability result on infini
te tree languages : it is decidable whether a Büchi language
is weak.
DTSTART;TZID=Europe/Paris:20130319T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201303191
100
UID:LSVsemLSV.201303191100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Hardware Design Automation - Problems\, Solutions & Scalabil
ity
STATUS:CONFIRMED
ATTENDEE;CN="Ulrich Kühne
":
MAILTO:no@spam.com
DESCRIPTION:
The size and complexity of integrated circuits has been grow
ing exponentially for decades. With this growing complexity\
, it is getting more and more challenging to organize the de
sign of hardware systems. Especially\, correctness is a cruc
ial issue\, since bugs that make it to the silicon can be ex
tremely expensive. Although for processors with over 3 billi
on transistors\, the use of formal methods seems to be out o
f range more than ever\, these methods are more and more use
d to accompany a quality driven design flow. This talk will
highlight some of the interesting problems occuring alongsid
e the different abstraction layers from the specification to
silicon\, like model checking\, verification coverage and d
ebugging. While there is a high degree of automation downwar
ds from hardware description languages such as VHDL or Veril
og\, a lot of manual work is still necessary on higher level
s of abstraction. Here\, natural language processing techniq
ues are a promising path towards improved design automation.
DTSTART;TZID=Europe/Paris:20130312T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201303121
100
UID:LSVsemLSV.201303121100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Checking NFA equivalence with bisimulations up to congruence
STATUS:CONFIRMED
ATTENDEE;CN="Damien Pous
":
MAILTO:no@spam.com
DESCRIPTION:
We introduce "bisimulation up to congruence" as a technique
for proving language equivalence of non-deterministic finite
automata. Exploiting this technique\, we devise an optimisa
tion of the classical algorithm by Hopcroft and Karp which\,
as we show\, is exploiting a weaker "bisimulation up to equ
ivalence" technique. The resulting algorithm can be exponent
ially faster than the recently introduced antichain algorith
ms. We actually show that antichain-based algorithms corresp
ond to using an up-to context technique\, so that our algori
thm can be seen as the result of merging both antichains and
Hopcroft and Karp's ideas.
DTSTART;TZID=Europe/Paris:20130226T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201302261
100
UID:LSVsemLSV.201302261100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Controller Synthesis Games
STATUS:CONFIRMED
ATTENDEE;CN="Marco Faella
":
MAILTO:no@spam.com
DESCRIPTION:
Games have been recognized as models of the interaction occu
rring between a plant and its environment\, both in the Comp
uter Science literature and in the Control Engineering one.
From the CS point of view\, the objective is to use game sol
ving algorithms to automatically synthesize controllers. In
this talk we will discuss what kind of games and solution co
ncepts are more appropriate for controller synthesis applica
tions. We will focus on two features that distinguish contro
ller synthesis games from most other games played in classic
al Game Theory and in Computer Science: first\, the fact tha
t the adversary is an indifferent environment; second\, the
importance of cost and performance measures\, such as the am
ount of memory needed by a controller to win a game.
DTSTART;TZID=Europe/Paris:20130219T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201302191
100
UID:LSVsemLSV.201302191100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
lAlBlC: a program testing the equivalence of dpda's
STATUS:CONFIRMED
ATTENDEE;CN="Géraud Sénizergues
":
MAILTO:no@spam.com
DESCRIPTION:
We present a preliminary version of the program "lAlBlC" (i.
e. lA=lB? let us Compute). The equivalence problem for dpda
consists in deciding\, for two given deterministic pushdown
automata A\,B\, whether they recognize the same language. It
was proved in [TCS 2001\, G.S.] that this problem is decida
ble by means of some complete proof systems. The program lAl
BlC gives\, in some sense\, life to the above completeness p
roof: on an input A\,B\, the program computes either a proof
of their equivalence (w.r.t. to the system D5 of the above
reference) or it computes a witness of their non-equivalence
(i.e. a word that belongs to the symmetric difference of th
e two languages). We shall outline the main mathematical obj
ects that are manipulated as well as the main functions perf
ormed over these objects. We shall emphasize the functionnal
style of the most abstract part of the program (synthesis o
f strategies from a sequence of tactics\, computation of a t
actics from a sequence of functions) as well as the algebrai
c structure that the basic objects are implementing: the gro
upoid of deterministic rational matrices over some structure
d alphabet. We shall also explain the experimental results o
btained so far (size of dpda's or grammars treated up to now
\, time and space of the computations\, size of the proofs).
The talk is based on an ongoing\, joint\, work with P. Henr
y.
DTSTART;TZID=Europe/Paris:20130129T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201301291
100
UID:LSVsemLSV.201301291100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
The Theory of Graph Games: Mixing Chess\, Soccer and Poker
STATUS:CONFIRMED
ATTENDEE;CN="Krishnendu Chatterjee
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk we will consider various classes of games playe
d on graphs with the classical objectives that are studied i
n the theory of verification. We will present a survey of re
sults for various different classes of game graphs and show
how more general class of games leads to more complicated re
sults. We will start with some basic and fundamental results
in game theory on graphs\, and then show how they can be ge
neralized to more different class of games.
DTSTART;TZID=Europe/Paris:20130115T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201301151
100
UID:LSVsemLSV.201301151100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
On the Formal Analysis of Physical Systems using Theorem Pro
ving
STATUS:CONFIRMED
ATTENDEE;CN="Vincent Aravantinos
":
MAILTO:no@spam.com
DESCRIPTION:
Formal methods have been used classically for the verificati
on of software\, circuits or protocols. In most cases\, veri
fication deals with an abstraction of the underlying physica
l system (e.g.\, software verification does not involve the
modelization of a computer\, circuit verification does not m
odel semi-conductors). We propose to try to verify such phys
ical systems\, focusing in particular on optical systems whi
ch have several applications (from fiber optics to quantum c
omputer implementations). This requires the formalization of
physical concepts (e.g. ray of light\, lens\, electromagnet
ic wave or photon)\, of the physical principles that govern
them (e.g.\, Fermat's principle or Maxwell equations)\, and
the derivation\, from these principles\, of various laws tha
t are useful for the verification of concrete systems (e.g.\
, Snell's law or the Uncertainty principle). We will explain
how these concepts and principles can be successfully forma
lized (in HOL-Light) as well as the limitations of this appr
oach.
DTSTART;TZID=Europe/Paris:20121218T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201212181
100
UID:LSVsemLSV.201212181100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Deciding the value 1 problem in one-player stochastic games
STATUS:CONFIRMED
ATTENDEE;CN="Hugo Gimbert
":
MAILTO:no@spam.com
DESCRIPTION:
A one-player game has value 1 if and only if the player has
strategies to win with probability arbitrarily close to 1. W
e survey known results about decidability and undecidability
of this problem and present a new class of partially observ
able Markov decision processes for which this problem is dec
idable.
DTSTART;TZID=Europe/Paris:20121212T140000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201212121
400
UID:LSVsemLSV.201212121400@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Modal Interface Automata
STATUS:CONFIRMED
ATTENDEE;CN="Walter Vogler
":
MAILTO:no@spam.com
DESCRIPTION:
De Alfaro and Henzinger's Interface Automata (IA) and Nyman
et al.'s recent combination IOMTS of IA and Larsen's Modal T
ransition Systems (MTS) are established frameworks for speci
fying interfaces of system components. However\, neither IA
nor IOMTS consider conjunction that is needed in practice wh
en a component satisfies multiple interfaces\, while Larsen'
s MTS-conjunction is not closed. In addition\, IOMTS-paralle
l composition exhibits a compositionality defect. In our wor
k\, we define conjunction (and also disjunction) on IA and M
TS and prove the operators to be `correct'\, i.e.\, the grea
test lower bounds (least upper bounds) with respect to IA- a
nd respectively MTS-refinement. As its main contribution\, a
novel interface theory called Modal Interface Automata (MIA
) is introduced: MIA is a rich subset of IOMTS\, is equipped
with compositional parallel\, conjunction and disjunction o
perators\, and allows a simpler embedding of IA than Nyman's
. Thus\, it fixes the shortcomings of related work\, without
restricting designers to deterministic interfaces as Raclet
et al.'s modal interface theory does.
DTSTART;TZID=Europe/Paris:20121212T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201212121
100
UID:LSVsemLSV.201212121100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Probabilistic modal mu-calculus with independent product
STATUS:CONFIRMED
ATTENDEE;CN="Matteo Mio
":
MAILTO:no@spam.com
DESCRIPTION:
The modal μ-calculus (Lμ) is the logic obtained by extending
standard propositional modal logic with least and greatest
fixed points operators. This logic was intensively studied i
n the last 30 years\, as it allows the expression of many in
teresting properties of labeled transition systems. The prob
abilistic modal Âµ-calculus (pLμ) is a generalization of Lμ\
, designed for expressing properties of probabilistic labele
d transition systems. In this talk I will discuss an extensi
on of pLμ\, called probabilistic modal μ-calculus with indep
endent product\, which can express more complex properties o
f practical interest. We provide two semantics for this exte
nded logic: one denotational and one based on a new kind of
games which we call Tree games. The main result is the equiv
alence of the two semantics. I will take the opportuninity\,
in the last part of the talk\, to discuss my current resear
ch in progress.
DTSTART;TZID=Europe/Paris:20121128T140000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201211281
400
UID:LSVsemLSV.201211281400@lsv.ens-cachan.fr
LOCATION:Salle Condorcet (Bât. d'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Towards Generating Compact Proof Certificates for Observatio
nal Equivalence
STATUS:CONFIRMED
ATTENDEE;CN="Alwen Tiu
":
MAILTO:no@spam.com
DESCRIPTION:
Observational equivalence\, in the context of process calcul
i\, is a notion of behavioral equivalence defined via observ
able actions of processes. It is commonly defined co-inducti
vely using the transitions of the processes\, and\, more imp
ortantly\, it needs to be closed under arbitrary process con
texts. Due to the latter requirement\, it is difficult to me
chanise observational equivalence checking directly\, and va
rious methods for approximating observational equivalence ha
ve been proposed in the literature. In this talk I will cons
ider an approximation of observational equivalence\, for the
spi-calculus\, based on labelled bisimulation\, and present
a procedure for checking this notion of bisimulation. This
procedure has been implemented in a logical framework called
Bedwyr. As the procedure and its implementation are quite c
omplex\, to increase confidence in the result of the impleme
ntion\, the prover (called SPEC) needs to produce an explici
t proof object\, in terms of a bisimulation set\, that can b
e checked independently outside the prover. Initial experime
nts suggest that often such a set can be very large\, even f
or simple processes. I will discuss several simplifications
to reduce the size of the bisimulation set that are currentl
y implemented in SPEC\, exploiting the so-called 'bisimulati
on-up-to' techniques\, originally developed by Milner\, Sang
iorgi and others for the pi-calculus. I will then discuss so
me directions for future work\, in particular incorporating
more general up-to techniques as logical theories in a logic
al framework.
DTSTART;TZID=Europe/Paris:20121204T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201212041
100
UID:LSVsemLSV.201212041100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Real-Time Scheduling on single processors - II
STATUS:CONFIRMED
ATTENDEE;CN="Giuseppe Lipari
":
MAILTO:no@spam.com
DESCRIPTION:
Real-Time scheduling deals with the problem of concurrently
executing processeses so that every process meets its timing
constraints. From the seminal work of Liu and Layland in 19
73\, concerning the scheduling of periodic real-time process
es on a single processor\, many researchers have extended th
e model and proposed alternative scheduling algorithms and s
chedulability analyses. The goal of this series of two semin
ars is to introduce the problem and give a quick overview of
the main results on real-time scheuling. In the second semi
nar\, I will address the problem of shared mutual exclusion.
I will discuss the Priority Inheritance\, Priority Ceiling
and Stack Resource Policy protocols. Then I will present som
e results on soft real-time scheduling and more specifically
Resource Reservation protocols. Finally\, I will present hi
erarchical scheduling\, and how to design a hierarchical sys
tem.
DTSTART;TZID=Europe/Paris:20121120T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201211201
100
UID:LSVsemLSV.201211201100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Real-Time Scheduling on single processors - I
STATUS:CONFIRMED
ATTENDEE;CN="Giuseppe Lipari
":
MAILTO:no@spam.com
DESCRIPTION:
Real-Time scheduling deals with the problem of concurrently
executing processeses so that every process meets its timing
constraints. From the seminal work of Liu and Layland in 19
73\, concerning the scheduling of periodic real-time process
es on a single processor\, many researchers have extended th
e model and proposed alternative scheduling algorithms and s
chedulability analyses. The goal of this series of two semin
ars is to introduce the problem and give a quick overview of
the main results on real-time scheuling. In the first semin
ar\, the problem of scheduling on a single resource (process
or) will be addressed. I will present the basic model for pe
riodic and sporadic tasks\, give a classification of the pro
blems and their complexity. I will also present analytical r
esults on schedulability analysis. The Fixed Priority and Ea
rlist Deadline First scheduling algorithm will be analysed i
n detail. During the seminar\, I will try to sketch a parall
el with model checking tools whenever possible.
DTSTART;TZID=Europe/Paris:20121113T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201211131
100
UID:LSVsemLSV.201211131100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
A Survey on Model-Checking Problems for Counter Automata
STATUS:CONFIRMED
ATTENDEE;CN="Christoph Haase
":
MAILTO:no@spam.com
DESCRIPTION:
Counter automata are a fundamental model of computation that
were introduced by Minsky sixty years ago. They comprise a
finite-state automaton with a finite number of counters rang
ing over the naturals. Along a transition\, a counter can be
incremented\, decremented\, or tested for zero. Minsky show
ed that the restriction to two counters suffices to render r
eachability undecidable. Due to this negative result\, vario
us restrictions on the the set of operations\, the underlyin
g graph structure\, the operation mode or the number of coun
ters have been considered in the literature and have shown t
o entail decidable reachability problems. Besides pure theor
etical interest\, those models have also found applications\
, for example in the verification of multi-threaded and conc
urrent programs\, programs with linked lists\, and modelling
of resource-bounded processes. Throughout the last ten year
s\, there has been a strong interest in model checking infin
ite graphs generated by subclasses of counter automata again
st specifications written in temporal logics. In this talk\,
I am going to give a high-level introduction to some of the
main concepts and ideas underlying the lower and upper boun
ds for various model checking problems with an emphasis on t
he restriction to one counter. It turns out that many proble
ms have beautiful connections to topics in number theory\, s
uch as non-linear Diophantine equations or Frobenius numbers
. I will also discuss some open problems and how they relate
to open problems in other areas. This talk is based on join
t work with Stefan Göller (Bremen)\, Stefan Kreutzer (Berlin
)\, and Joel Ouaknine and James Worrell (Oxford).
DTSTART;TZID=Europe/Paris:20121009T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201210091
100
UID:LSVsemLSV.201210091100@lsv.ens-cachan.fr
LOCATION:Salle Condorcet (Bât. d'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Achieving Accuracy and Strong Data Protection Using Differen
tial Privacy
STATUS:CONFIRMED
ATTENDEE;CN="Gerome Miklau
":
MAILTO:no@spam.com
DESCRIPTION:
The goal of private statistical data analysis is to permit t
he accurate analysis of a group of individuals while protect
ing the personal information of each individual. Differentia
l privacy provides a formal basis for achieving these seemin
gly contradictory goals. It is a rigorous privacy standard t
hat protects against powerful adversaries\, offers precise a
ccuracy guarantees\, and has been successfully applied to a
range of data analysis tasks. When differential privacy is s
atisfied\, individuals in a dataset enjoy the compelling ass
urance that information released about the dataset is virtua
lly indistinguishable whether or not their personal data is
included. Differential privacy is achieved by introducing ra
ndomness into query answers. A major goal of research in thi
s area is to devise methods that offer the best accuracy for
a fixed level of privacy. After reviewing the basic princip
les of differential privacy\, I will describe how query cons
traints and statistical inference can be used to construct a
more accurate differentially-private algorithms\, with no p
rivacy penalty. The example application comes from our recen
t work investigating the properties of a social network that
can be studied without threatening the privacy of individua
ls and their connections. I will show that the degree distri
bution of a network can be estimated privately and accuratel
y by asking a special query for which constraints are known
to hold\, and then exploiting the constraints to infer a mor
e accurate final result.
DTSTART;TZID=Europe/Paris:20121002T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201210021
100
UID:LSVsemLSV.201210021100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Asynchronous Games over Tree Architectures
STATUS:CONFIRMED
ATTENDEE;CN="Anca Muscholl
":
MAILTO:no@spam.com
DESCRIPTION:
We consider the control problem for Zielonka asynchronous au
tomata. This is a distributed synthesis problem since Zielon
ka automata is an asynchronous parallel composition of finit
e processes communicating via rendez-vous. The most importan
t aspect of this model is that the processes participating i
n a rendez-vous can exchange complete information about thei
r causal past. It is an intriguing open problem whether the
control problem is decidable in this setting. We show decida
bility of the control problem for Zielonka automata over an
acyclic communication architecture. The complexity of our al
gorithm is l-fold exponential with l being the height of the
tree representing the architecture. We show that this compl
exity is tight. This is joint work with B. Genest\, H. Gimbe
rt and I. Walukiewicz.
DTSTART;TZID=Europe/Paris:20120626T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201206261
100
UID:LSVsemLSV.201206261100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Using automata to compute prefix and infix probabilities
STATUS:CONFIRMED
ATTENDEE;CN="Mark-Jan Nederhof
":
MAILTO:no@spam.com
DESCRIPTION:
With a given probabilistic grammar\, the notion of a prefix
or an infix probability of a string was motivated by applica
tions in speech recognition and machine translation. Until r
ecently\, the only known solutions allowed to compute the pr
efix probability with context-free and tree-adjoining gramma
rs. We show that a much wider class of problems allow straig
htforward solutions by considering intersection with regular
languages.
DTSTART;TZID=Europe/Paris:20120612T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201206121
100
UID:LSVsemLSV.201206121100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
L'informatique en France depuis 1962: d'une "science incerta
ine" à une discipline établie. L'exemple de l'ENSET-ENS Cach
an
STATUS:CONFIRMED
ATTENDEE;CN="Pierre Mounier-Kuhn
":
MAILTO:no@spam.com
DESCRIPTION:
En dépouillant archives et revues scientifiques\, on découvr
e que la France est le seul pays industrialisé où la recherc
he publique n'a pas réussi à construire d'ordinateur dans la
période pionnière\, avant 1960. L'informatique s'y est cepe
ndant développée grâce aux initiatives d'universitaires\, vé
ritables entrepreneurs de science\, souvent en Province\, qu
i collaboraient avec des industriels novateurs et avec les a
dministrations techniques civiles ou militaires. Ils ont dû
bientÃ´t faire face à l'explosion de la demande du marché du
travail\, qui réclamait toujours plus d'informaticiens. Au
cours des années 1960-1970\, on est passé progressivement du
calcul électronique\, outil au service des ingénieurs et de
s mathématiques appliquées\, à une discipline nouvelle\, l'i
nformatique\, qui recomposait le paysage scientifique. Cette
évolution ne s'est pas accomplie sans résistances et polémi
ques. Comment l'école normale supérieure de l'enseignement t
echnique (ENSET)\, devenue école normale supérieure de Cacha
n\, s'est-elle comportée face au développement rapide de cet
te discipline\, qui correspondait à la fois à une demande so
cio-économique en forte expansion et à une priorité politiqu
e affirmée par une succession de plans gouvernementaux ? Des
questions plus précises peuvent Ãªtre formulées\, concernan
t à la fois l'école et ses principaux partenaires dans l'adm
inistration et l'enseignement: Selon quel processus l'inform
atique s'est-elle établie à l'ENSET\, suivant quels modèles
et sous quelles formes : calcul et mathématiques appliquées\
, électronique et automatisme\, bureautique et gestion ? Com
ment la création du CAPET Informatique et d'une section info
rmatique à l'école\, à la fin des années 1960\, s'articula-t
-elle avec la politique générale de formation en ce domaine
? Comment l'école a-t-elle "géré" son évolution face aux mut
ations du travail\, des modes de production\, du changement
technique dans l'industrie et dans le tertiaire ? Si l'infor
matique a été dès les années 1950 un domaine où les femmes p
ouvaient percer professionnellement plus que dans des techni
ques traditionnelles\, l'école a-t-elle pris en compte cette
possibilité par exemple en s'appuyant sur sa filière commer
ciale déjà nettement féminisée ? Quelle dynamique de recherc
he aboutit à la fondation du laboratoire LSV en 1997 ?
DTSTART;TZID=Europe/Paris:20120522T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201205221
100
UID:LSVsemLSV.201205221100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Quotienting out Persistent Singletons
STATUS:CONFIRMED
ATTENDEE;CN="Tobias Heindel
":
MAILTO:no@spam.com
DESCRIPTION:
Persistent sets are a cornerstone of Partial Order Reduction
; however\, they need to be combined with additional methods
(such as sleep sets) to avoid the state-space-explosion pro
blem\, e.g.\, in deadlock detection. However\, one crucial f
act is that persistent *singletons* are "inessential" in a s
uitable\, technical sense; thus\, the goal is to eliminate t
hem "directly". Roughly\, we can render asynchronous transit
ion systems more compact by "quotienting out" all persistent
singletons\, using techniques of directed algebraic topolog
y. The talk illustrates the crucial ideas for the case of oc
currence nets and focuses on the relation to Haar's facet ab
straction.
DTSTART;TZID=Europe/Paris:20120417T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201204171
100
UID:LSVsemLSV.201204171100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Anonymous Authentication in Cryptographic Protocols
STATUS:CONFIRMED
ATTENDEE;CN="Malika Izabachene
":
MAILTO:no@spam.com
DESCRIPTION:
Anonymity arises in several contexts\, in e-voting systems\,
e-payment transactions\, location-based services\, and more
generally in situations where an identity service provides
some authorization to users. In this talk\, I will give a fe
w illustrations of some technical issues for anonymous authe
ntication in both the interactive and non-interactive settin
gs. As a first step\, I will review security notions and con
structions for anonymous encryption schemes and will propose
applications to provable-secure password-based key-exchange
protocols. I will then introduce anonymous credentials\, wh
ich are signatures enabling users to authenticate later on t
o some service provider without revealing any information ab
out them. I will finally present an efficient provable-secur
e e-cash system as one of its many applications.
DTSTART;TZID=Europe/Paris:20120412T140000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201204121
400
UID:LSVsemLSV.201204121400@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Methods for Enumeration
STATUS:CONFIRMED
ATTENDEE;CN="Yann Strozecki
":
MAILTO:no@spam.com
DESCRIPTION:
I will present enumerations problems\, that is we want to pr
oduce the set of solutions of a problem. Several methods to
design low complexity enumeration algorithms will be present
ed. In these settings we want both the total time and the de
lay between two solutions to be small. First we will use rep
resentation of combinatorial problems by polynomial to reduc
e enumeration to multivariate interpolation. This leads to p
robabilistic algorithms for problems on graphs\, hypergraphs
\, probabilistic automata ... Queries over databases or tree
s are natural examples of enumeration problems. I will prese
nt first-order queries with free second-order variables and
explain how to solve them when their quantifier depth is sma
ll. We are also interested in a verification problem: findin
g witnesses that two systems (automata\, MDP ...) are differ
ent. Since the number of witnesses may be infinite\, their e
numeration is not possible. Thus we try to sample them unifo
rmly using random walks on polytopes.
DTSTART;TZID=Europe/Paris:20120411T140000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201204111
400
UID:LSVsemLSV.201204111400@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Queue-Dispatch Asynchronous Systems
STATUS:CONFIRMED
ATTENDEE;CN="Alexander Heußner
":
MAILTO:no@spam.com
DESCRIPTION:
To make the development of efficient multi-core applications
easier\, libraries\, such as Grand Central Dispatch (GCD)\,
have been proposed. In GCD\, the programmer separtes its co
de into chunks\, i.e.\, functionally separate units\, so-cal
led blocks\, and dispatches them\, using synchronous or asyn
chronous calls\, to several types of waiting queues. An OS-l
evel scheduler is then responsible for dispatching those blo
cks on the available cores. In addition to synchronization b
y synchronous calls\, all running blocks can synchronize via
global memory. Thus\, GCD and similar libraries permit comp
lex patterns of causal interaction between concurrently runn
ing blocks and stronlgy require the help of formal methods t
o assure correctness criteria for GCD-based programs. We pro
pose Queue-Dispatch Asynchronous Systems (QDAS) as a mathema
tical model that faithfully formalizes the synchronization m
echanisms and the behavior of the scheduler in those systems
. This allows to uncover the relationship of this type of mo
dels to classical ones such as pushdown systems\, Petri nets
\, fifo systems\, and counter systems. Our main technical co
ntributions are precise worst-case complexity results for th
e Parikh coverability problem for several subclasses of our
model. We further give an outlook on ongoing and future work
that focusses approximative approaches to verification and
the addition of quantitative aspects. This is joint work wit
h Gilles Geeraerts and Jean-François Raskin.
DTSTART;TZID=Europe/Paris:20120410T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201204101
100
UID:LSVsemLSV.201204101100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Logics on Trees
STATUS:CONFIRMED
ATTENDEE;CN="Amélie Gheerbrant
":
MAILTO:no@spam.com
DESCRIPTION:
The talk will present and relate results from two different
papers: On the Complexity of Query Answering over Incomplete
XML Documents (joint with L. Libkin and T. Tan)\, Proceedin
gs of ICDT 2012. Complete Axiomatizations of fragments of MS
O on Finite Trees (joint work with B. ten Cate)\, to appear
in LMCS. The first paper provides complete axiomatizations o
f fragments of MSO on finite node-labelled sibling-ordered t
rees. In order to prove completeness\, model-theoretic tools
specifically geared towards Henkin models are developed (e.
g. Ehrenfeucht-Fraïssé games and Feferman-Vaught theorems).
The second paper studies the data and combined complexity of
query answering over incomplete XML documents\, completing
the picture of previous studies by examining more expressive
languages and other semantic assumptions. A new tractable c
lass of FO queries is identified both for the relational and
XML case: Boolean combinations of existential positive quer
ies (under open and closed world assumptions). The results a
re obtained via a new technique which has a model-theoretic
flavor\, whereas automata-theoretic techniques are usually p
redominant in the study of XML. I will take the occasion to
emphasize and discuss the use of model-theoretic techniques
in the study of logics on trees.
DTSTART;TZID=Europe/Paris:20120403T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201204031
100
UID:LSVsemLSV.201204031100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Formal Proofs of Robustness for Watermarking Algorithms
STATUS:CONFIRMED
ATTENDEE;CN="David Baelde
":
MAILTO:no@spam.com
DESCRIPTION:
I will present some new results on the security of watermark
ing schemes against arbitrary attackers\, and their full for
malization in Coq. This is joint work with P. Courtieu\, D.
Gross-Amblard and C. Paulin\, as part of the ANR project Sca
lp which focuses on formal proofs of probabilistic algorithm
s. Watermarking techniques are used to help identifying copi
es of publicly released information. They consist in applyin
g a slight and secret modification to the data before its re
lease\, in a way that should be robust\, ie.\, remain recogn
izable even in (reasonably) modified copies of the data. We
present new results about the robustness of watermarking sch
emes against arbitrary attackers\, and the formalization of
those results in Coq. We used the ALEA library\, which forma
lizes probability theory and models probabilistic programs u
sing a simple monadic translation. This work illustrates the
strengths and particularities of the induced style of reaso
ning about probabilistic programs. Our technique for proving
robustness is adapted from methods commonly used for crypto
graphic protocols\, and we discuss its relevance to the fiel
d of watermarking.
DTSTART;TZID=Europe/Paris:20120322T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201203221
100
UID:LSVsemLSV.201203221100@lsv.ens-cachan.fr
LOCATION:Salle Renaudeau (Bâtiment Laplace)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Automatic verification of heap-manipulating sequential progr
ams with unbounded data
STATUS:CONFIRMED
ATTENDEE;CN="Cezara Drăgoi
":
MAILTO:no@spam.com
DESCRIPTION:
We develop a logic-based framework for the automatic verific
ation of sequential programs manipulating dynamic data struc
tures carrying unbounded data. We are interested in proving
safety specifications\, that describe the structure of the a
llocated memory\, its size and also the values of the data f
ields. To this we have considered a framework where sets of
configurations are represented by formulas in first order lo
gic with reachability predicates. First\, we investigated th
e automation of pre/post-condition reasoning. We introduced
a multi-sorted first order logic that has a decidable satisf
iability problem and it is closed under the computation of t
he strongest post-condition. This logic combines reachabilit
y predicates that are used to describe the structure of the
allocated memory\, linear constraints to describe its size a
nd formulas in a first order logic over the data domain to c
onstrain the values of the data fields. Second\, to increase
the level of automation we address the issue of synthesizin
g assertions for programs with singly-linked lists. These as
sertions represent over-approximations of the program's set
of reachable states. We define an abstract interpretation ba
sed framework which combines a specific finite-range abstrac
tion on the structure of the allocated memory with an abstra
ct domain on sequences of data.
DTSTART;TZID=Europe/Paris:20120320T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201203201
100
UID:LSVsemLSV.201203201100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
A tetrachotomy for positive equality-free logic
STATUS:CONFIRMED
ATTENDEE;CN="Barnaby Martin
":
MAILTO:no@spam.com
DESCRIPTION:
We consider the problem of evaluating positive equality-free
sentences of FO on a fixed\, finite relational structure B.
This may be seen as a generalisation of the Quantified Cons
traint Satisfaction Problem (QCSP)\, itself a generalisation
of the Constraint Satisfaction Problem (CSP). We argue that
our generalisation is not totally arbitrary\, and that ours
is the only problem in a large class - other than the CSP a
nd QCSP - whose complexity taxonomy was unsolved. We introdu
ce surjective hyper-endomorphisms in order to give a Galois
connection that characterises definability in positive equal
ity-free FO. Through the algebraic method we are able to cha
racterise the complexity of our problem for all finite struc
tures B. Specifically\, the problem is either in Logspace\,
NP-complete\, co-NP-complete or Pspace-complete. The problem
appears obtuse\, but possesses a surprising elegance. There
may yet be lessons to be learnt in the methodology of the s
olution of this case\, for the continuing program for CSP.
DTSTART;TZID=Europe/Paris:20120312T140000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201203121
400
UID:LSVsemLSV.201203121400@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Order-2 morphic words and recursion schemes
STATUS:CONFIRMED
ATTENDEE;CN="Laurent Braud
":
MAILTO:no@spam.com
DESCRIPTION:
We investigate the infinite-words which are frontiers of sol
utions of recursive schemes\, i.e. leaves by lexicographic o
rder of infinite trees. For order-1 schemes\, they are exact
ly the morphic words\, i.e. images of fixpoints of morphisms
of words. We extend this result to solutions of order-2 sch
emes\, and introduce 2-morphic words. Safety is not a restri
ction when considering a specific tree shape\, so these word
s are exactly the words of the corresponding level in the pu
shdown hierarchy and enjoy the associated properties.
DTSTART;TZID=Europe/Paris:20120306T140000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201203061
400
UID:LSVsemLSV.201203061400@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Exploiting Structure in LTL Synthesis
STATUS:CONFIRMED
ATTENDEE;CN="Emmanuel Filiot
":
MAILTO:no@spam.com
DESCRIPTION:
The aim of program synthesis is to automatically generate a
program that satisfies a given specification\, in contrast t
o program verification\, for which both the specification an
d the program are given as input. The underlying goal is to
improve program reliability and optimize design constraints\
, like time and human errors\, and to get rid of the low-lev
el programming tasks\, by replacing them with the design of
high-level specifications. The old dream of automatic synthe
sis\, which among others was shared by Church\, is difficult
to realize for general-purpose programming languages. Howev
er in recent years\, there has been a renewed interest in fe
asible methods for the synthesis of application specific pro
grams\, which have been\, for instance\, applied to reactive
systems\, distributed systems\, programs manipulating arith
metic or concurrent data-structures. Reactive systems are no
n-terminating programs that continuously interact with their
environment. They arise both as hardware and software\, and
are usually part of safety-critical systems\, for example m
icroprocessors\, air traffic controllers\, programs to monit
or medical devices\, or nuclear plants. It is therefore cruc
ial to guarantee their correctness. The temporal logic LTL i
s a very important abstract formalism to describe properties
of reactive systems. As shown by Pnueli and Rosner in 89\,
the synthesis of reactive systems from LTL specifications is
a 2-Exptime complete problem. In this talk\, I will present
recent progresses in LTL synthesis based on a bounded synth
esis approach inspired by bounded model-checking\, and show
that the high worst-case time complexity of LTL synthesis do
es not handicap its practical feasibility. This is achieved
by exploiting the structure underlying the automata construc
tions used to solve the synthesis problem.
DTSTART;TZID=Europe/Paris:20120306T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201203061
100
UID:LSVsemLSV.201203061100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Channel Synthesis for Finite Transducers
STATUS:CONFIRMED
ATTENDEE;CN="Mathieu Sassolas
":
MAILTO:no@spam.com
DESCRIPTION:
We investigate how two agents can communicate through a nois
y medium modeled as a finite transducer. In terms of securit
y\, this communication -- if unintended by the system's desi
gner -- can be seen as an information leak through the syste
m. The sender and the receiver are also described by finite
transducers which can respectively encode and decode binary
messages. When the communication is reliable\, modulo some t
ransmission delay or errors\, we call the encoder/decoder pa
ir a channel. We study the channel synthesis problem\, which
asks whether\, given a system\, such sender and receiver ex
ist and builds them if the answer is positive. We prove that
the problem is undecidable. However\, when the transducer i
s functional\, we obtain a synthesis procedure based on a st
ructural property. This is joint work with Gilles Benattar\,
Béatrice Bérard\, Didier Lime\, John Mullins and Olivier H.
Roux.
DTSTART;TZID=Europe/Paris:20120228T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201202281
100
UID:LSVsemLSV.201202281100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Tolerating Transient\, Permanent\, and Intermittent Failures
STATUS:CONFIRMED
ATTENDEE;CN="Swan Dubois
":
MAILTO:no@spam.com
DESCRIPTION:
When the size of a distributed system gets larger or when it
is deployed in hazardous environments\, the possibility tha
t some elements of the system are subject to faults (failure
\, memory corruption\, hacking\, ...) become impossible to e
lude. Faults can be classified according to duration\, span\
, or nature. In this talk\, we focus on distributed systems
that simultaneously tolerate several kinds of faults using t
hree classical problems as case studies. We present first a
distributed protocol simulating a single-writer multi-reader
atomic register in the presence of transient faults and of
permanent crash faults. This protocol relies on two re-usabl
e tools: a communication primitive and a bounded timestamp s
cheme. Then\, we study logical clock weak synchronization in
the presence of transient faults and of intermittent Byzant
ine faults. We prove several impossibility results and provi
de a protocol that is optimal both with respect to impossibi
lity result and with respect to recovery time. Finally\, we
define three new fault tolerance schemes in distributed syst
ems that are subject to transient faults and to intermittent
Byzantine faults. We design a protocol constructing a wide
class of spanning trees that is optimal with respect to faul
t tolerance metrics defined for these three schemes.
DTSTART;TZID=Europe/Paris:20120216T140000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201202161
400
UID:LSVsemLSV.201202161400@lsv.ens-cachan.fr
LOCATION:Salle Condorcet (Bâtiment d'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Better abstractions for timed automata
STATUS:CONFIRMED
ATTENDEE;CN="B Srivathsan
":
MAILTO:no@spam.com
DESCRIPTION:
We consider the reachability problem for timed automata. A s
tandard solution to this problem involves computing a search
tree whose nodes are abstractions of zones. These abstracti
ons preserve underlying simulation relations on the state sp
ace of the automaton. For both effectiveness and efficiency
reasons\, they are parametrized by the maximal lower and upp
er bounds (LU-bounds) occurring in the guards of the automat
on. We consider the A-lu abstraction defined by Behrmann et
al. Since this abstraction can potentially yield non-convex
sets\, it has not been used in implementations. We prove tha
t A-lu abstraction is the biggest abstraction with respect t
o LU-bounds that is sound and complete for reachability. We
also provide an efficient technique to use the A-lu abstract
ion to solve the reachability problem. Joint work with Frédé
ric Herbreteau and Igor Walukiewicz.
DTSTART;TZID=Europe/Paris:20120214T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201202141
100
UID:LSVsemLSV.201202141100@lsv.ens-cachan.fr
LOCATION:Amphithéâtre Tocqueville
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Counter-Example Guided Fence Insertion under TSO
STATUS:CONFIRMED
ATTENDEE;CN="Mohamed Faouzi Atig
":
MAILTO:no@spam.com
DESCRIPTION:
We consider the reachability problem for concurrent finite-s
tate programs running under the classical TSO memory model.
This model allows "write to read" relaxation corresponding t
o the addition of an unbounded store buffer between each pro
cessor and the main memory. We show that the reachability pr
oblem for a program under TSO is decidable. Then\, we propos
e a counter-example guided fence insertion procedure. The pr
ocedure is augmented by a placement constraint that allows t
he user to choose places inside the program where fences may
be inserted. For a given placement constraint\, we automati
cally infer all minimal sets of fences that ensure correctne
ss. We have implemented a prototype and run it successfully
on all standard benchmarks together with several challenging
examples that are beyond the applicability of existing meth
ods. [This talk will be based on: (1) POPL'10 paper with Ahm
ed Bouajjani\, Burckhardt and Madanlal Musuvathi\, and (2) T
ACAS'12 paper with Parosh Abdulla\, Yu-Fang Chen\, Carl Leon
ardsson and Ahmed Rezine]
DTSTART;TZID=Europe/Paris:20120131T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201201311
100
UID:LSVsemLSV.201201311100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Component-based analysis of real-time systems
STATUS:CONFIRMED
ATTENDEE;CN="Giuseppe Lipari
":
MAILTO:no@spam.com
DESCRIPTION:
The complexity of modern embedded real-time systems is const
antly increasing\, as new and more complex functionality is
added to existing software. At the same time\, due to the in
creasing computational power of the hardware platforms and t
o the pressure to reduce the costs\, software that in the pa
st was run on different computational nodes\, is now being i
ntegrated onto a single node. An appealing way to reduce com
plexity is to apply a component-based real-time design metho
dology. A real-time system can be seen as a set of interacti
ng components\, each one providing a well-defined subset of
functionalities\, whose integration produces the final syste
m behavior. A component-based methodology is successful only
if it can effectively reduce the complexity. To achieve thi
s goal\, the system designer must be able to 1) analyze and
validate each component in isolation from the rest of the sy
stem\, 2) summarize its properties and requirements into sim
pler interfaces\, 3) perform the final integration analysis
and validation on the component interfaces. In this talk\, t
he author will give an overview of current techniques for co
mponent-based analysis of real-time systems\, with a look at
their possible use in avionics and automotive systems. Then
\, a possible research agenda will be discussed\, highlighti
ng the shortcomings of current analysis and how to improve o
n it.
DTSTART;TZID=Europe/Paris:20120124T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201201241
100
UID:LSVsemLSV.201201241100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Everlasting Security through Quantum Cryptography
STATUS:CONFIRMED
ATTENDEE;CN="Dominique Unruh
":
MAILTO:no@spam.com
DESCRIPTION:
Cryptography is a powerful tool for processing confidential
data. Cryptographic protocols are\, however\, only as secure
as the underlying encryption schemes. And we do not know wh
ether these might not be broken at some point in the future.
This leaves us in a difficult situation: If we process high
ly sensitive data using cryptographic protocols\, an attacke
r might simply record all messages. Should the underlying en
cryption scheme be broken in the future\, the attacker will
then be able to decrypt all confidential data in retrospect.
For highly confidential data (such as\, e.g.\, medical reco
rds) such a situation is not acceptable. A way out is "everl
asting security". A protocol with everlasting security guara
ntees that all data involved in the protocol stays secure\,
even if at some point in the future all the underlying encry
ption schemes are broken. Unfortunately\, with traditional c
ryptographic techniques\, everlasting security can only be a
chieved in very limited situations. In this talk\, we explai
n how everlasting security can be achieved for a wide variet
y of tasks by using quantum cryptography\, i.e.\, by making
use of quantum mechanical effects in the cryptographic proto
col.
DTSTART;TZID=Europe/Paris:20120117T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201201171
100
UID:LSVsemLSV.201201171100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Cryptanalysis
STATUS:CONFIRMED
ATTENDEE;CN="Pierre-Alain Fouque
":
MAILTO:no@spam.com
DESCRIPTION:
Cryptanalysis is a set of methods to circumvent the security
of cryptographic algorithms. It can be applied at different
levels: at the assumption level\, attacking the computation
ally-hard problem on which the security of a scheme is based
; at the scheme level\, attacking the scheme directly when i
ts security is not based on some hard problems (this is the
case when specific instances of a hard problems are used) or
in symmetric cryptography; finally at the implementation le
vel\, when side channel information can be used. In this tal
k\, I will make a survey of some cryptanalytic techniques an
d describe my contributions towards this field.
DTSTART;TZID=Europe/Paris:20111129T140000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201111291
400
UID:LSVsemLSV.201111291400@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Uniform strategies
STATUS:CONFIRMED
ATTENDEE;CN="Sophie Pinchinat
":
MAILTO:no@spam.com
DESCRIPTION:
Imperfect information games are becoming very popular for th
eir ability to model interaction under uncertainty. Examples
of this kind of situations are many\, e.g. distributed feat
ures of computing systems\, attacker's dialog with a securit
y system\, etc. Also\, such games naturally arise in logic\,
e.g. as satisfiability games for mu-calculus formulas. Rece
ntly\, some kind of imperfect information games have been us
ed to provide the semantics of logics\, as for Dependence Lo
gic. We propose the notion of "uniform strategy" which unifi
es the aforementioned approaches\, and even provides new mod
el-checking games for complex logics\, e.g. combining time a
nd knowledge. Our definition relies on pairs of parameters :
an equivalence relation between plays\, and a uniformity co
ndition over sets of equivalent plays. Basically\, a strateg
y is uniform if the equivalence class of any play induced by
the strategy satisfies the uniformity condition. For exampl
e\, the equivalence can arise from a player ability to obser
ve and recall what happened during the play (The perfect rec
all-imperfect recall spectrum lies in this parameter). Addit
ionally\, the uniformity condition can express many aspects.
It can capture the nature of the strategy\, e.g. that it is
observation-based\, as needed in the very standard imperfec
t information games setting. It can characterize non-regular
properties of strategies\, e.g. that strategies maintain th
e opponent's uncertainty about some secret\, as considered i
n games with opacity condition. In this talk\, we will expla
in and motivate our notion of uniform strategy\, and relate
it to various examples from the literature: namely\, imperfe
ct information games\, games with opacity condition\, emptin
ess of alternating automata\, first-order dependence logic m
odel-checking games\, epistemic temporal logic model-checkin
g games. If time left\, we will address decidability and com
plexity issues by scanning computational hypothesis one may
require on the pair of parameters.
DTSTART;TZID=Europe/Paris:20111129T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201111291
100
UID:LSVsemLSV.201111291100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
The Computational Complexity of Verifying One-Counter Proces
ses
STATUS:CONFIRMED
ATTENDEE;CN="Stefan Göller
":
MAILTO:no@spam.com
DESCRIPTION:
A one-counter automaton is a pushdown automaton over a singl
eton stack alphabet plus a bottom-of-stack symbol. I will ta
lk about equivalence checking and model checking of processe
s generated by one-counter automata\, so-called one-counter
processes (OCPs). The goal of the talk is to present some id
eas and techniques that are used for obtaining complexity bo
unds for these problems. In the first part of the talk I pla
n to show that it is PSPACE-complete to decide strong bisimu
lation equivalence for OCPs. The previously best known upper
bound for this problem was 3-EXPSPACE. The same problem tur
ns out to be NL-complete when the processes are described by
deterministic one-counter automata. In the second part of t
he talk\, I plan to discuss a technique for proving lower bo
unds by employing two known results from complexity theory:
(i) Converting a natural number in Chinese remainder present
ation into binary presentation is in logspace-uniform NC^1 a
nd (ii) PSPACE is AC^0-serializable. With the latter one can
prove that there exists a fixed CTL formula for which model
checking of OCPs is PSPACE-hard. With the same technique on
e can show some further lower bounds\, as for example the fo
llowing one: The emptiness problem for timed automata with t
wo clocks but with modulo tests is PSPACE-complete even if a
ll numbers are encoded in unary. The results were obtained i
n joint works with Stanislav Böhm\, Petr Jancar and Markus L
ohrey.
DTSTART;TZID=Europe/Paris:20111122T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201111221
100
UID:LSVsemLSV.201111221100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Symbolic Methods for the Automatic Search of Attacks Against
Some Block Ciphers
STATUS:CONFIRMED
ATTENDEE;CN="Charles Bouillaguet
":
MAILTO:no@spam.com
DESCRIPTION:
The block cipher cryptanalyst usually faces the following pr
oblem: she may interact with a black box containing the bloc
k cipher instantiated with a secret random key\, and her goa
l is\, in most cases\, to retrieve this secret key using les
s time than exhaustive search and asking less encryptions/de
cryptions to the black box than the whole codebook. Several
researchers had previously observed that the Advanced Encryp
tion Standard (AES)\, the most widespread block cipher\, had
a relatively simple algebraic description over the field wi
th 256 elements\, because of its byte-oriented design. Howev
er\, this property has not been harnessed by cryptanalysts t
o this day. In particular the (tempting) approach consisting
in writing down the equations describing the AES\, and tryi
ng to solve them directly using off-the-shelf tools such as
SAT-solvers\, has systematically failed to provide any resul
t. In this talk\, I will present the results we obtained usi
ng a slightly different method. We have designed tools that
take as input a system of AES-like equations\, and that sear
ch for an efficient ad hoc solving procedure. The result of
these tools is the source code of a solver that can only sol
ve the input system\, but which can in some cases be efficie
nt (its complexity can be predicted accurately). This solver
can then be compiled and run to find the actual solutions.
Our tools\, which "reason" from the equations describing the
AES (or similar looking symmetric primitives) are intrinsic
ally symbolic\, and they are inspired by standard tools from
the field of automated deduction\, such as the DPLL algorit
hm for SAT\, the Knuth-Bendix completion algorithm\, or the
resolution algorithm for first-order logic. These tools foun
d\, nearly automatically\, the best known Low-Data-Complexit
y attacks on reduced versions of the AES\, and the best know
n attack on the full versions of AES-derived primitives\, su
ch as the Message Authentication code Pelican-MAC\, and the
stream cipher LEX.
DTSTART;TZID=Europe/Paris:20111115T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201111151
100
UID:LSVsemLSV.201111151100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Logico-Numerical Abstract Acceleration and Application to th
e Verification of Data-Flow Programs
STATUS:CONFIRMED
ATTENDEE;CN="Peter Schrammel
":
MAILTO:no@spam.com
DESCRIPTION:
We are interested in the verification of safety properties a
bout synchronous data-flow programs with Boolean and numeric
al variables\, e.g.\, Lustre programs. We rely on reachable-
state analysis for this problem. Two main techniques for ens
uring the termination of such an analysis are acceleration a
nd widening (within the abstract interpretation framework).
Acceleration-based methods lead to exact results\, but they
guarantee termination only for a restricted class of program
s. Widening is less precise and less predictable but does no
t have this limitation. Abstract acceleration integrates acc
eleration techniques into the abstract interpretation framew
ork\, such as to reduce the need for widening and thus to im
prove precision. All these techniques however require the en
umeration of the Boolean state-space\, which leads to a stat
e-space explosion even for medium-sized Lustre programs. In
this talk we propose a solution by extending numerical accel
eration to logico-numerical acceleration. We define logico-n
umerical abstract acceleration methods based on a partial de
coupling of Boolean and numerical transitions and we show ho
w well-chosen partitioning techniques make them effective. E
xperimental results show that incorporating these methods in
a verification tool based on abstract interpretation provid
es not only significant advantage in terms of precision\, bu
t also a gain in performance.
DTSTART;TZID=Europe/Paris:20111108T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201111081
100
UID:LSVsemLSV.201111081100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Toward Machine-Checked Program Verification for Concrete Cry
ptography
STATUS:CONFIRMED
ATTENDEE;CN="Pierre-Yves Strub
":
MAILTO:no@spam.com
DESCRIPTION:
Type systems\, relational logics\, and interactive proof ass
istants are effective tools for verifying the security of pr
ograms and systems that rely on cryptography. They can provi
de automation\, modularity and scalability. As illustrated i
n recent case studies\, they can be usefully applied to larg
e security protocols and applications [Bhargavan et al.\, 20
08\, Fournet et al.\, 2009]. However\, their models traditio
nally rely on abstract assumptions on the underlying cryptog
raphic primitives\, expressed in symbolic models. Cryptograp
hers usually reason on security assumptions in lower-level m
odels that precisely account for the complexity and probabil
ity of attacks. These models are more complex and realistic\
, but recent results suggest thay they are also amenable to
formal automated verification [Blanchet\, 2006\, Barthe et a
l.\, 2009\, Acar et al.\, 2011]. I will present our on-going
work in adapting and extending our programming and verifica
tion framework based on refinement types for ML programs [Be
ngtson et al.\, 2008\, Bhargavan et al.\, 2010\, Fournet\, 2
011] which currently uses a combination of automated proofs
(using Z3\, an SMT solver) and interactive proofs (using Coq
)\, in order to produce machine-checked security proofs of c
ryptographic programs and libraries under concrete computati
onal assumptions. This work is part of the “Secure Distribut
ed Computations” group of the “MSR-INRIA Joint Centre”.
DTSTART;TZID=Europe/Paris:20110927T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201109271
100
UID:LSVsemLSV.201109271100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Keeping track of your friends and enemies: privacy threats o
f new mobile technologies
STATUS:CONFIRMED
ATTENDEE;CN="Myrto Arapinis
":
MAILTO:no@spam.com
DESCRIPTION:
Joint work with Loretta Mancini\, Eike Ritter\, and Mark Rya
n. The proliferation of portable computing devices\, such as
mobile phones\, Bluetooth devices\, and RFID tags\, has lea
d to a range of new computer security problems. In order to
fulfil their goals\, these devices need to report our moveme
nts to service providers such as mobile phone network operat
ors\, banks\, and governments. While most of users accept th
at the service providers can track their physical movements\
, few would be happy if an arbitrary third party could do so
. Such a possibility would enable all kinds of undesirable b
ehaviours\, ranging from criminal stalking to more mundane m
onitoring of spouse or employee movements. For this reason\,
protocols have been designed to prevent third parties from
identifying wireless messages as coming from a particular us
er. These protocols usually include cryptography and make us
e of temporary identifiers\, in an effort to achieve the aim
of untraceability by third parties. At CSF'10\, we presente
d a formal framework for analysing untraceability/unlinkabil
ity in the applied pi calculus. We used our framework to sho
w that French e-Passports are traceable\, while British ones
aren't. In this talk\, I will present you our work on the a
nalysis of Universal Mobile Telecommunication System (UMTS)
protocols. I will show you a problem we have identified with
the UMTS authentication and key establishment protocol: alt
hough mobile phones use temporary identities to identify the
mselves to the Network\, a replayed message can be used to i
dentify a particular mobile phone. Our attack exploits the f
act that the victim's phone will reply with subtly different
error messages\, depending on whether the replayed request
is associated with it or with a different phone. To thwart t
his attack\, we propose a modification of the protocol\, and
verify the proposed fix using our framework and the ProVeri
f tool.
DTSTART;TZID=Europe/Paris:20110920T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201109201
100
UID:LSVsemLSV.201109201100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Verification of Ad hoc Networks: Unreliability and Time
STATUS:CONFIRMED
ATTENDEE;CN="Giorgio Delzanno
":
MAILTO:no@spam.com
DESCRIPTION:
In the first part of the talk we present an analysis of veri
fication problems\, formulated as parameterized reachability
\, for an abstract model of Ad Hoc Network protocols in pres
ence of node and communication failures. We consider here di
fferent types of failures: intermittency\, crash and restart
of single nodes\, loss and conflicts of broadcast messages.
In the second part we present an extension of the model in
which nodes are specified by timed automata and\, for the ne
w model\, discuss parameterized reachability problems for di
fferent classes of topologies.
DTSTART;TZID=Europe/Paris:20110712T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201107121
100
UID:LSVsemLSV.201107121100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Reasoning about Web Security
STATUS:CONFIRMED
ATTENDEE;CN="Tamara Rezk
":
MAILTO:no@spam.com
DESCRIPTION:
Mixing existing online libraries and data into new online ap
plications in a rapid\, inexpensive manner\, often referred
to as mashups\, has captured the way of designing web applic
ations. In this talk\, I will: overview security vulnerabili
ties that arise from web applications specificities such as
code injection and gadget inclusion; and describe proposals
based on language-based security approaches.
DTSTART;TZID=Europe/Paris:20110705T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201107051
100
UID:LSVsemLSV.201107051100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Coalgebraic Logics and Tableaux
STATUS:CONFIRMED
ATTENDEE;CN="Clemens Kupke
":
MAILTO:no@spam.com
DESCRIPTION:
Many of the logics that are used in computer science today a
re variations of modal logics as they offer a good compromis
e between expressive power on the one hand\, and good algori
thmic properties on the other hand. Extensions of basic moda
l logic are obtained by allowing for ontological reasoning (
description logics) and by adding the ability to specify ong
oing\, possibly infinite behaviour (fixpoint logics). Other
variations of basic modal logic are designed to fit specific
semantic domains such as modal logics for Markov chains\, g
ame frames or neighbourhood structures. In my talk I am goin
g to present coalgebraic modal logic as a general framework
in which the above mentioned variations of basic modal logic
can be studied in a uniform way. In particular\, I am going
to describe tableau calculi that yield generic decidability
proofs for the coalgebraic mu-calculus and coalgebraic desc
ription logics. As corollaries we obtain previously unknown
Exptime-decidability results for these logics.
DTSTART;TZID=Europe/Paris:20110614T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201106141
100
UID:LSVsemLSV.201106141100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Beyond Control-State Reachability for Communicating Pushdown
Systems
STATUS:CONFIRMED
ATTENDEE;CN="Alexander Heußner
":
MAILTO:no@spam.com
DESCRIPTION:
Pushdown systems synchronizing by unbounded\, reliable fifo
queues seem a quite natural model for distributed systems th
at communicate via TCP or MPI. Recent publications focus on
the influence of constraining the network architecture on ba
sic decidability questions\, but do not allow to derive posi
tive results beyond control-state reachability when assuming
syntactic and semantic restrictions that are still "applica
ble" in practice. We present first ideas on leaving behind i
nterleaving semantics in order to verify MSO properties base
d on a graph grammar based representation of a system's part
ial-order behaviour.
DTSTART;TZID=Europe/Paris:20110531T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201105311
100
UID:LSVsemLSV.201105311100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Assembling Sessions
STATUS:CONFIRMED
ATTENDEE;CN="Madhavan Mukund
":
MAILTO:no@spam.com
DESCRIPTION:
Sessions are a central paradigm in Web services\, as they al
low the implementation of decentralized transactions with mu
ltiple participants. Sessions enable the cooperation of work
flows while at the same time avoiding the mixing of workflow
s from distinct transactions. Several languages such as BPEL
\, ORC\, AXML have been proposed to implement Web Services.
Sessions are usually implemented by attaching unique identif
iers to transactions. The expressive power of these language
s makes the properties of the implemented services undecidab
le. In this talk\, we propose a new formalism for modelling
web services. Our model is session-based\, but avoids using
session identifiers. The model can be translated to a dialec
t of Petri nets that allows the verification of important pr
operties of web services in terms of coverability in Petri n
ets. This is joint work with Philippe Darondeau and Loic Hel
ouet.
DTSTART;TZID=Europe/Paris:20110524T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201105241
100
UID:LSVsemLSV.201105241100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Approximating Hybrid Systems
STATUS:CONFIRMED
ATTENDEE;CN="Mahesh Viswanathan
":
MAILTO:no@spam.com
DESCRIPTION:
he widespread deployment of computing devices that manage an
d control physical processes in safety critical environments
\, has made their analysis and verification a very important
problem. Since formal models that disregard the physical pr
ocesses tend to be conservative and suboptimal\, the most po
pular way to model and analyze such systems is using hybrid
systems\, that have finitely many control states to model di
screte behavior and finitely many real valued variables that
evolve continuously with time to model the interaction with
the physical world. Despite considerable progress in the la
st couple of decades\, the automated verification of cyber p
hysical systems remains stubbornly challenging. In this talk
we will discuss one approach to making the analysis more sc
alable\, namely\, by automatically constructing "simpler"\,
"smaller" models\, and then analysing these approximated mod
els. We will present a couple of techniques to approximate h
ybrid models\, based on the Stone-Weierstrauss Theorem and c
ounter-example guided abstraction-refinement (CEGAR)\, and d
iscuss their applications to automated verification.
DTSTART;TZID=Europe/Paris:20110517T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201105171
100
UID:LSVsemLSV.201105171100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Towards better tools for the analysis and quality assurance
of FOSS distributions
STATUS:CONFIRMED
ATTENDEE;CN="Ralf Treinen
":
MAILTO:no@spam.com
DESCRIPTION:
Free and Open Source Software (FOSS) distributions are among
the largest and fastest moving existing component-based sof
tware distributions\, which poses interesting challenges bot
h for the quality assurance process of distributions as for
the management of individual installations. The first part o
f this talk will give an overview of some of the results obt
ained in the EDOS and Mancoosi European projects on the anal
ysis of inter-package relationships. We will focus on the to
ols that came out of these research projects\, and discuss t
he way how these are currently put to use. In the second par
t of the talk I will present recent results on deciding prop
erties that range over all possible future evolutions of a c
urrent component repository. The properties we are intereste
d in concern the coherent component installations permitted
in any future. We show that a certain class of these propert
ies can be decided by checking a finite set of repositories
that is representative for the infinite set of all possible
futures. We discuss our implementation of tools checking two
particular instances of this schema.
DTSTART;TZID=Europe/Paris:20110426T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201104261
100
UID:LSVsemLSV.201104261100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Playing games when states have rich structure
STATUS:CONFIRMED
ATTENDEE;CN="Lukasz Kaiser
":
MAILTO:no@spam.com
DESCRIPTION:
Both in the classical theory of extensive-form games and in
the more recent theory of games on graphs it is normally ass
umed that a state of the game has no structure beyond the ou
tgoing moves. In other words\, the internal structure of the
states is abstracted away. This is very useful in some case
s\, but can be a hindrance in others\, for example when stud
ying games on pushdown graphs or on timed automata. To bette
r understand how internal structure of the states can influe
nce behaviour of the players\, we introduce a general model
of games with structured states. In our model\, actions of t
he players are given by structure rewriting rules and winnin
g conditions by logic formulas. In case of games with perfec
t information\, we show that the structure of the states can
be exploited to create simple strategies\, sometimes even w
hen the number of states in the game is infinite. This is si
milar to games on pushdown graphs and indeed\, we prove a cl
ose relationship between pushdown games and our model when r
ewriting rules are of a certain simple form.
DTSTART;TZID=Europe/Paris:20110412T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201104121
100
UID:LSVsemLSV.201104121100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Pattern-based Verification for Multithreaded Programs
STATUS:CONFIRMED
ATTENDEE;CN="Pierre Ganty
":
MAILTO:no@spam.com
DESCRIPTION:
Pattern-based verification checks the correctness of the pro
gram executions that follow a given pattern\, a regular expr
ession over the alphabet of program transitions of the form
w1* ... wn*. For multithreaded programs\, the alphabet of th
e pattern is given by the synchronization operations between
threads. After introducing the model\, we study the complex
ity of pattern-based verification for abstracted multithread
ed. While unrestricted verification is undecidable for abstr
acted multithreaded programs with recursive procedures and P
SPACE-complete for abstracted multithreaded while-programs\,
we show that pattern-based verification is NP-complete for
both classes. Using recent results about Parikh images of co
ntext-free languages and semilinear sets\, we show that patt
ern-based verification becomes polynomial when the number of
threads\, the longest acyclic path in the call graph\, and
the size of the pattern are fixed\, but the procedures can s
till be arbitrarily large.
DTSTART;TZID=Europe/Paris:20110405T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201104051
100
UID:LSVsemLSV.201104051100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Entropy of timed languages
STATUS:CONFIRMED
ATTENDEE;CN="Eugene Asarin
":
MAILTO:no@spam.com
DESCRIPTION:
For timed languages\, we define measures of their size: volu
me for a fixed finite number of events\, and entropy (growth
rate) as asymptotic measure for an unbounded number of even
ts. These measures can be used for comparison of languages\,
and the entropy can be viewed as information contents of a
timed language. In case of languages of deterministic timed
automata\, we give exact formulas for volumes. Next we chara
cterize the entropy\, using methods of functional analysis\,
as a logarithm of the leading eigenvalue (spectral radius)
of a positive integral operator. We devise several methods t
o compute the entropy: a symbolical one for so-called "1 1/2
-clock" automata\, and two numerical ones: one using techniq
ues of functional analysis\, another based on discretization
. (The talk is based on Concur'09\, FORMATS'09\, FSTTCS'10 a
rticles with Aldric Degorre)
DTSTART;TZID=Europe/Paris:20110322T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201103221
100
UID:LSVsemLSV.201103221100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Residuation of tropical series: rationality issues
STATUS:CONFIRMED
ATTENDEE;CN="Anne Bouillard
":
MAILTO:no@spam.com
DESCRIPTION:
Decidability of existence\, rationality of delay controllers
and robust delay controllers are investigated for systems w
ith time weights in the tropical and interval semirings. Dep
ending on the (max\,+) or (min\,+)-rationality of the series
specifying the controlled system and the control objective\
, cases are identified where the controller series defined b
y residuation is rational\, and when it is positive (i.e.\,
when delay control is feasible). When the control objective
is specified by a tolerance\, i.e. by two bounding rational
series\, a nice case is identified in which the controller s
eries is of the same rational type as the system specificati
on series.
DTSTART;TZID=Europe/Paris:20110308T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201103081
100
UID:LSVsemLSV.201103081100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
A Logical Framework for Capturing the Dynamics of Informatio
n and Abilities of Players in Multi-Player Games: a prelimin
ary report
STATUS:CONFIRMED
ATTENDEE;CN="Valentin Goranko
":
MAILTO:no@spam.com
DESCRIPTION:
I will discuss first steps towards a more realistic treatmen
t and logical formalization of the abilities of players to a
chieve objectives in multi-player games under incomplete\, i
mperfect\, or simply wrong information that they may have ab
out the game and about the course of the play. In this talk\
, after some motivating examples I will introduce a variatio
n of the multi-agent logic ATL as a logical framework for ca
pturing the interplay between the dynamics of information an
d the dynamics of abilities of players. This framework takes
into account both the a priori information of players with
respect to the game structure and the empirical information
that players develop over the course of an actual play. It a
ssociate with them respective information relations and noti
ons of `a priori' and `empirical' strategies and strategic a
bilities. I will discuss the problem of model checking of st
atements formalized in the new logic under different assumpt
ions about the abilities of the players to observe\, remembe
r\, and reason. Most of the talk will be based on a joint wo
rk with Peter Hawke (now at Stanford Univ.)
DTSTART;TZID=Europe/Paris:20110222T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201102221
100
UID:LSVsemLSV.201102221100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Proving that programs eventually do something good
STATUS:CONFIRMED
ATTENDEE;CN="Byron Cook
":
MAILTO:no@spam.com
DESCRIPTION:
Software failures can be sorted into two groups: those that
cause the software to do something wrong (e.g. crashing)\, a
nd those that result in the software not doing something use
ful (e.g. hanging). In recent years automatic tools have bee
n developed which use mathematical proof techniques to certi
fy that software cannot crash. But\, based on Alan Turing's
proof of the halting problem's undecidablity\, many have con
sidered the dream of automatically proving the absence of ha
ngs to be impossible. While not refuting Turing's original r
esult\, recent research now makes this dream a reality. This
lecture will describe this recent work and its application
to industrial software. Bio: Dr. Byron Cook is a Principal R
esearcher at Microsoft Research in Cambridge\, UK as well as
Professor of Computer Science at Queen Mary\, University of
London. He is one of the developers of the Terminator progr
am termination proving tool\, as well as the SLAM software m
odel checker. See research.microsoft.com/~bycook/ for more i
nformation.
DTSTART;TZID=Europe/Paris:20110218T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201102181
100
UID:LSVsemLSV.201102181100@lsv.ens-cachan.fr
LOCATION:Amphithéâtre Marie Curie (Bâtiment d'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Recursion Schemes and their Automata Models
STATUS:CONFIRMED
ATTENDEE;CN="Olivier Serre
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk\, I will present two equi-expressive models for
generating infinite trees. The first one are higher-order r
ecursion schemes\, which can be thought as a deterministic r
ewriting system over terms (essentially\, the simply-typed l
ambda calculus with recursion). The second one are higher-or
der pushdown automata\, which are an extension of pushdown a
utomata that uses stacks of stacks instead of stacks of symb
ols. The first part of the talk will be devoted to present t
he models and give examples. The second part\, will focus on
properties of the trees generated by such models (in partic
ular\, the decidability of the monadic second order logic)\,
and will illustrate the advantages of automata techniques w
hen working with such objects.
DTSTART;TZID=Europe/Paris:20110215T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201102151
100
UID:LSVsemLSV.201102151100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Temporal logics over linear time domains are in PSPACE
STATUS:CONFIRMED
ATTENDEE;CN="Alexander Rabinovich
":
MAILTO:no@spam.com
DESCRIPTION:
We investigate the complexity of the satisfiability problem
of temporal logics with a finite set of modalities. We show
that the problem is in PSPACE over the class of all linear o
rders\, over rationals\, over the reals and over many intere
sting classes of linear orders.
DTSTART;TZID=Europe/Paris:20110125T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201101251
100
UID:LSVsemLSV.201101251100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Symbolic Techniques in Propositional Satisfiability Solving
STATUS:CONFIRMED
ATTENDEE;CN="Moshe Y. Vardi
":
MAILTO:no@spam.com
DESCRIPTION:
Search-based techniques in propositional satisfiability (SAT
) solving have been enormously successful\, leading to what
is becoming known as the "SAT Revolution". Essentially all s
tate-of-the-art SAT solvers are based on the Davis-Putnam-Lo
gemann-Loveland (DPLL) technique\, augmented with backjumpin
g and conflict learning. Much of current research in this ar
ea involves refinements and extensions of the DPLL technique
. Yet\, due to the impressive success of DPLL\, little effor
t has gone into investigating alternative techniques. This w
ork focuses on symbolic techniques for SAT solving\, with th
e aim of stimulating a broader research agenda in this area.
Refutation proofs can be viewed as a special case of constr
aint propagation\, which is a fundamental technique in solvi
ng constraint-satisfaction problems. The generalization lift
s\, in a uniform way\, the concept of refutation from Boolea
n satisfiability problems to general constraint-satisfaction
problems. On the one hand\, this enables us to study and ch
aracterize basic concepts\, such as refutation width\, using
tools from finite-model theory. On the other hand\, this en
ables us to introduce new proof systems\, based on represent
ation classes\, that have not been considered up to this poi
nt. We consider ordered binary decision diagrams (OBDDs) as
a case study of a representation class for refutations\, and
compare their strength to well-known proof systems\, such a
s resolution\, the Gaussian calculus\, cutting planes\, and
Frege systems of bounded alternation-depth. In particular\,
we show that refutations by ODBBs polynomially simulate reso
lution and can be exponentially stronger. We then describe a
n effort to turn OBDD refutations into OBBD decision procedu
res. The idea of this approach\, which we call "symbolic qua
ntifier elimination"\, is to view an instance of proposition
al satisfiability as an existentially quantified proposition
al formula. Satisfiability solving then amounts to quantifie
r elimination; once all quantifiers have been eliminated we
are left with either 1 or 0. Our goal here is to study the e
ffectiveness of symbolic quantifier elimination as an approa
ch to satisfiability solving. To that end\, we conduct a dir
ect comparison with the DPLL-based ZChaff\, as well as evalu
ate a variety of optimization techniques for the symbolic ap
proach. In comparing the symbolic approach to ZChaff\, we ev
aluate scalability across a variety of classes of formulas.
We find that no approach dominates across all classes. While
ZChaff dominates for many classes of formulas\, the symboli
c approach is superior for other classes of formulas. Finall
y\, we turn our attention to Quantified Boolean Formulas (QB
F) solving. Much recent work has gone into adapting techniqu
es that were originally developed for SAT solving to QBF sol
ving. In particular\, QBF solvers are often based on SAT sol
vers. Most competitive QBF solvers are search-based. Here we
describe an alternative approach to QBF solving\, based on
symbolic quantifier elimination. We extend some symbolic app
roaches for SAT solving to symbolic QBF solving\, using vari
ous decision-diagram formalisms such as OBDDs and ZDDs. In b
oth approaches\, QBF formulas are solved by eliminating all
their quantifiers. Our first solver\, QMRES\, maintains a se
t of clauses represented by a ZDD and eliminates quantifiers
via multi-resolution. Our second solver\, QBDD\, maintains
a set of OBDDs\, and eliminate quantifiers by applying them
to the underlying OBDDs. We compare our symbolic solvers to
several competitive search-based solvers. We show that QBDD
is not competitive\, but QMRESS compares favorably with sear
ch-based solvers on various benchmarks consisting of non-ran
dom formulas.
DTSTART;TZID=Europe/Paris:20101103T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201011031
100
UID:LSVsemLSV.201011031100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
On probabilistic regular graphs
STATUS:CONFIRMED
ATTENDEE;CN="Christophe Morvan
":
MAILTO:no@spam.com
DESCRIPTION:
Regular graphs (generated by deterministic graph grammars) f
orm a simple and natural generalisation of pushdown automata
. In this talk we use such graphs to define infinite state M
arkov chains. We establish some model checking results for a
probabilistic temporal logic (pCTL). These results were alr
eady known for probabilistic pushdown automata\, but we advo
cate that regular graphs enable a simpler exposition. This i
s joint work with Nathalie Bertrand (INRIA Rennes).
DTSTART;TZID=Europe/Paris:20101116T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201011161
100
UID:LSVsemLSV.201011161100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Parameterized Verification of Ad Hoc Networks
STATUS:CONFIRMED
ATTENDEE;CN="Arnaud Sangnier
":
MAILTO:no@spam.com
DESCRIPTION:
We study decision problems for parameterized verification of
a formal model of Ad Hoc Networks with selective broadcast.
The communication topology of a network is represented as a
graph. Nodes represent states of individual processes. Adja
cent nodes represent single-hop neighbors. Processes are fin
ite state automata that communicate via selective broadcast
messages. Reception of a broadcast is restricted to single-h
op neighbors. For this model we consider verification proble
ms that can be expressed as reachability of configurations w
ith one node (resp. all nodes) in a certain state from an in
itial configuration with an arbitrary number of nodes and un
known topology. We are interested in decision problems that
are parametric on the size and on the shape of the communica
tion topology of the initial configurations. We draw a compl
ete picture of the decidability boundaries of these problems
according to different assumptions on the mobility of the n
odes in the networks and on the form of the communication gr
aphs. This a joint work with Giorgio Delzanno (University of
Genova) and Gianluigi Zavattaro (University of Bologna).
DTSTART;TZID=Europe/Paris:20101019T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201010191
100
UID:LSVsemLSV.201010191100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
OPA -- reconquering the web
STATUS:CONFIRMED
ATTENDEE;CN="David Rajchenbach-Teller
":
MAILTO:no@spam.com
DESCRIPTION:
For many\, the Web is Wikipedia\, Google Maps and hundreds o
f other rich applications\, both powerful and usable from an
ywhere. For others\, it is a security nightmare\, full of ho
les\, both low-level and high-level\, exploited or waiting t
o be exploited. And for developers\, it is a heap of dozens
of distinct technologies\, often approximative\, incompatibl
e\, which need to be configured individually\, connected man
ually\, often blindly and without clear semantics. In such c
onditions\, nothing can be checked or verified. In this talk
\, we present OPA\, a new approach for web programming\, bas
ed on semantics and type systems. OPA is a programming langu
age\, grounded in lambda-calculus and pi-calculus\, designed
for the web\, for databases\, for concurrency and for distr
ibution. One unique language for the whole application\, wit
h formal semantics\, simple primitives\, a clear syntax\, an
d safety and security guarantees. Oh\, and a few proofs in C
oq.
DTSTART;TZID=Europe/Paris:20100914T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201009141
100
UID:LSVsemLSV.201009141100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Composable symbolic security definitions
STATUS:CONFIRMED
ATTENDEE;CN="Dominique Unruh
":
MAILTO:no@spam.com
DESCRIPTION:
The definition of Universal Composability (UC; Canetti\, FOC
S 2001) is a cryptographic security definition that is both
simple and gives very strong security guarantees. In particu
lar\, it ensures that the composition of secure protocols st
ays secure. The idea of UC is not\, however\, restricted to
the cryptographic (computational) setting; instead\, one can
see it as a refinement relation on protocols and programs t
hat preserves security and is composable. We show how UC can
be applied in a symbolic security setting. We also show a n
ew design technique (virtual primitives). This design techni
que allows to circumvent\, in a symbolic UC setting\, variou
s impossibility results that apply in the cryptographic sett
ing.
DTSTART;TZID=Europe/Paris:20100629T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201006291
100
UID:LSVsemLSV.201006291100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
The Tree-Width of the Auxiliary Storage
STATUS:CONFIRMED
ATTENDEE;CN="Gennaro Parlato
":
MAILTO:no@spam.com
DESCRIPTION:
The talk is about a generalization of various results on the
decidability of emptiness for several restricted classes of
sequential and distributed automata with auxiliary storage
(stacks\, queues) that have recently been proved. Our genera
lization relies on reducing emptiness of these automata to f
inite-state *graph automata* (without storage) defined on mo
nadic second-order (MSO) definable graphs of bounded tree-wi
dth\, where the graph structure encodes the mechanism provid
ed by the auxiliary storage. Our results outline a uniform m
echanism to derive emptiness algorithms for automata\, expla
ining and simplifying several existing results\, as well as
proving new decidability theorems.
DTSTART;TZID=Europe/Paris:20100601T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201006011
100
UID:LSVsemLSV.201006011100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Constrained Environment Assumptions for Multi-Threaded Progr
ams
STATUS:CONFIRMED
ATTENDEE;CN="Andrey Rybalchenko
":
MAILTO:no@spam.com
DESCRIPTION:
Automated verification of multi-threaded programs requires e
xplicit identification of the interplay between interacting
threads\, so-called environment assumptions\, to enable scal
able reasoning. Once identified\, these assumptions can be u
sed for reasoning with one program thread at a time\, which
is possible by using the respective environment assumption t
o model the interleaving with other threads. Finding adequat
e assumptions that are sufficiently precise to yield conclus
ive results and yet keep track only of necessary facts about
the execution environment in order to scale well is a major
challenge. In this talk I will present a constraint-based t
echnique for the inference of such assumptions. Our techniqu
e automatically steers towards an optimal precision/efficien
cy trade-off between the extremes of efficient\, but incompl
ete thread-modular reasoning and complete\, but prohibitivel
y expensive consideration of all interleavings. For this tas
k\, we pinpoint a declarative formulation of modular verific
ation that allows one to express requisite environment assum
ptions using constraints and admits algorithmic solutions ba
sed on abstract fixpoint checking. I will describe an applic
ation of our environment assumption inference for the verifi
cation of reachability and termination properties of multi-t
hreaded programs. Joint work with Ashutosh Gupta and Corneli
u Popeea
DTSTART;TZID=Europe/Paris:20100330T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201003301
100
UID:LSVsemLSV.201003301100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
What's in a Name? Evaluating (and Possibly Improving) the Se
curity and Usability of Personal Knowledge Questions
STATUS:CONFIRMED
ATTENDEE;CN="Mike Just
":
MAILTO:no@spam.com
DESCRIPTION:
Authentication systems that rely upon personal knowledge que
stions (such as "What is your mother's maiden name?") are wi
dely used but have\, until recently\, received little attent
ion from the academic community. In this talk\, I will prese
nt several methods and results regarding the security and us
ability of these authentication questions. Evaluating securi
ty has\, on one hand\, involved adapting techniques from gue
ssing theory and applying them to real-world statistical dis
tributions for typical answer categories such as the names o
f people\, pets and places. It can also involve staging expe
riments where friends or family members are encouraged to gu
ess answers. Experiments can also be used to evaluate the us
ability (e.g.\, memorability) of challenge questions and the
ir answers. And while the results of existing personal knowl
edge question systems have been mostly negative\, some possi
ble improvements might be gained through increased interacti
on with the user\, for example\, to shape the answer distrib
ution and lower the prevalence of common answers\, or to int
roduce more tolerant authentication so as to reduce the reli
ance on perfect response accuracy.
DTSTART;TZID=Europe/Paris:20100608T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201006081
100
UID:LSVsemLSV.201006081100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Programmes de branchement pour l'évaluation d'arbres
STATUS:CONFIRMED
ATTENDEE;CN="Pierre McKenzie
":
MAILTO:no@spam.com
DESCRIPTION:
Après un retour sur le "pebbling"\, sur le modèle du program
me de branchement et sur sa relation avec la machine de Turi
ng\, je présenterai des bornes inférieures sur la taille de
programmes de branchement résolvant le problème de l'évaluat
ion d'un arbre (je préciserai ce problème\, qui rappelle la
faÃ§on dont un "treillis automaton" effectue son calcul). Tr
avaux effectués avec Mark Braverman\, Steve Cook\, Rahul San
thanam et Dustin Wehr\, présentés à MFCS 2009 et FSTTCS 2009
.
DTSTART;TZID=Europe/Paris:20100427T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201004271
100
UID:LSVsemLSV.201004271100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
On Weak Modal Compatibility and Refinement of Modal I/O Tran
sition Systems
STATUS:CONFIRMED
ATTENDEE;CN="Rolf Hennicker
":
MAILTO:no@spam.com
DESCRIPTION:
Modal I/O automata (MIOs) by Larsen et al. provide a flexibl
e framework for the specification and implementation of inte
racting systems. They distinguish between "may" transitions
and "must" transitions\, where the former can be disregarded
and the latter must be respected by any correct refinement.
Building on the theory of MIOs we introduce a new compatibi
lity notion\, called weak modal compatibility\, for interact
ing components. As an important property of behavioural inte
rface theories we prove that weak modal compatibility is pre
served under weak modal refinement. Then we extend the notio
n of weak modal compatibility to loosely coupled systems whi
ch interact via buffered FIFO channels. We show that also in
this case weak compatibility is preserved by weak modal ref
inement and that\, moreover\, local refinements compose to g
lobal refinements. Finally\, we describe the MIO Workbench\,
an Eclipse-based editor and verification tool for modal I/O
automata.
DTSTART;TZID=Europe/Paris:20100511T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201005111
100
UID:LSVsemLSV.201005111100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
On cycles and separability of persistent Petri nets
STATUS:CONFIRMED
ATTENDEE;CN="Philippe Darondeau
":
MAILTO:no@spam.com
DESCRIPTION:
We show that PBRP nets (plain\, bounded\, reversible and per
sistent Petri nets) have bases of cycles made of transition
disjoint cycles. We show that PBRP nets are strongly separab
le\, meaning that a PBRP net whose initial marking is of the
form k.M may be simulated by k replicas of this net\, each
with initial marking M. We show that if a net with initial m
arking k.M is PBRP then the similar net with initial marking
(k-1).M is also PBRP. (joint work with Eike Best)
DTSTART;TZID=Europe/Paris:20100525T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201005251
100
UID:LSVsemLSV.201005251100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
From Counter Abstraction to Thread-State Cutoffs: New Techni
ques for Multi-Threaded Program Verification
STATUS:CONFIRMED
ATTENDEE;CN="Thomas Wahl
":
MAILTO:no@spam.com
DESCRIPTION:
The formal analysis of multi-threaded programs is among the
grand challenges of software verification research. In this
talk\, I describe our recent and ongoing work on analyzing p
arameterized finite-state programs\, such as non-recursive m
ulti-threaded Boolean programs\, a principal ingredient in p
redicate abstraction. I begin with a scalable method for ana
lyzing the reachability of program locations in programs exe
cuted by a bounded number of threads. This method\, being ba
sed on counter abstraction\, extends in principle to unbound
ed thread counts\, but suffers in practice from the high com
plexity of coverability and reachability analyses for certai
n types of counter machines. A different approach to program
location reachability rests on the assumption that in pract
ical parametric program settings\, a small "cutoff" number o
f threads suffice to generate all reachable program location
s. While this assumption is widely considered to be safe\, i
ts practical usefulness hinges on how accurately we are able
to estimate the cutoff of a given program. I present a new
method that analyses the reachable state space of a replicat
ed finite-state program for increasing thread counts\, until
a condition emerges that allows us to conclude that the cut
off thread count has been reached. Completeness of this meth
od is achieved by resorting to traditional coverability anal
yses in corner cases. The result is a precise and efficient
program location reachability method for replicated finite-s
tate programs run by arbitrarily many threads.
DTSTART;TZID=Europe/Paris:20100420T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201004201
100
UID:LSVsemLSV.201004201100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
(Un)decidability in Petri nets with name creation and replic
ation
STATUS:CONFIRMED
ATTENDEE;CN="Fernando Rosa Velardo
":
MAILTO:no@spam.com
DESCRIPTION:
The study of the expressive power of computation models in
between Petri nets and Turing machines\, and in particular o
f the class of Well Structured Transition Systems\, is a cha
llenging research problem. In this talk I will present two o
rthogonal extensions of Petri nets\, with the capability of
creating and managing pure names\, and with a replication pr
imitive\, getting ν-Petri nets and g-RN systems\, respective
ly. First\, I will show how these two extensions are strongl
y equivalent\, but only when a garbage collection mechanism
is added for idle threads. However\, when both extensions ar
e considered simultaneously\, we obtain a Turing complete mo
del\, that we call ν-RN systems. Then I will survey the know
n expressivity results for ν-Petri nets (and therefore\, for
g-RN systems). In particular\, coverability\, boundedness a
nd termination are decidable\, while reachability and place-
boundedness are undecidable\, so that ν-Petri nets are stric
tly in between Petri nets and Turing machines. Then I will s
how how can we restrict ν-Petri nets (and\, therefore\, g-RN
systems) and ν-RN systems in order to keep decidability of
reachability and coverability\, respectively. In particular\
, if we forbid synchronizations between the different compon
ents in a g-RN system\, then reachability is still decidable
. Analogously\, if we forbid name communication between the
different components in a ν-RN system\, or restrict communic
ation to happen only for a given finite set of names\, we ob
tain decidability of coverability. Finally\, I will comment
on some ongoing work. This is joint work with David de Fruto
s-Escrig. http://kimba.mat.ucm.es/~frosa/publicaciones#fi08
DTSTART;TZID=Europe/Paris:20100209T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201002091
100
UID:LSVsemLSV.201002091100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Electing a University President using Open-Audit Voting
STATUS:CONFIRMED
ATTENDEE;CN="Olivier Pereira
":
MAILTO:no@spam.com
DESCRIPTION:
In March 2009\, the Université catholique de Louvain elected
its President using a custom deployment of the Helios web-b
ased open-audit voting system. Out of 25\,000 potential vote
rs\, 5000 registered\, and almost 4000 voted in each round o
f the election. The precision of the voting system turned ou
t to be crucial: in the first round\, the leader came short
of winning the election by only 2 votes. We will describe th
e Helios-based voting system used in this election\, the spe
cifics of the UCL deployment\, and the lessons learned in th
is deployment. We note at least one interesting conclusion:
while it is often assumed that open-audit voting will lead t
o more complaints and potentially a denial-of-service attack
on the auditing process\, we found that\, instead\, complai
nts are likely to be more easily handled in open-audit elect
ions because evidence and counter-evidence can be presented.
This is joint work with Ben Adida and Olivier de Marneffe.
DTSTART;TZID=Europe/Paris:20100309T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201003091
100
UID:LSVsemLSV.201003091100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Modular Verification of Security Protocol Code by Typing
STATUS:CONFIRMED
ATTENDEE;CN="Karthik Bhargavan
":
MAILTO:no@spam.com
DESCRIPTION:
TBA
DTSTART;TZID=Europe/Paris:20100126T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201001261
100
UID:LSVsemLSV.201001261100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Machines Reasoning about Machines
STATUS:CONFIRMED
ATTENDEE;CN="J Strother Moore
":
MAILTO:no@spam.com
DESCRIPTION:
Computer hardware and software can be modeled precisely in m
athematical logic. If expressed appropriately\, these models
can be executable. An appropriate logic is an axiomatically
formalized functional programming language. This allows mod
els to be used as simulation engines or rapid prototypes. Bu
t because they are formal they can be manipulated by symboli
c means: theorems can be proved about them\, directly\, with
mechanical theorem provers. But how practical is this visio
n of machines reasoning about machines? In this highly perso
nal talk\, I will describe the 40 year history of the Boyer-
Moore Project and discuss progress toward making formal veri
fication practical. Among other examples I will describe imp
ortant theorems about commercial microprocessor designs\, in
cluding parts of processors by AMD\, Motorola\, IBM\, Rockwe
ll-Collins and others. Some of these microprocessor models e
xecute at 90% the speed of C models and have had important f
unctional properties verified. In addition\, I will describe
a model of the Java Virtual Machine\, including class loadi
ng and bytecode verification and the proofs of theorems abou
t JVM methods. Biography J Strother Moore holds the Admiral
B.R. Inman Centennial Chair in Computing Theory at the Unive
rsity of Texas at Austin. He is the author of many books and
papers on automated theorem proving and mechanical verifica
tion of computing systems. Along with Boyer he is a co-autho
r of the Boyer-Moore theorem prover and the Boyer-Moore fast
string searching algorithm. With Matt Kaufmann he is the co
-author of the ACL2 theorem prover. Moore got his SB from MI
T in 1970 and his PhD from the University of Edinburgh in 19
73. Moore was a founder of Computational Logic\, Inc.\, and
served as its chief scientist for ten years. He served as ch
air of the UT Austin CS department for eight years. He and B
ob Boyer were awarded the McCarthy Prize in 1983 and the Cur
rent Prize in Automatic Theorem Proving by the American Math
ematical Society in 1991. In 1999\, they were awarded the He
rbrand Award for their work in automatic theorem proving. Bo
yer\, Moore\, and Kaufmann were awarded the 2005 ACM Softwar
e Systems Award for the Boyer-Moore theorem prover. Moore is
a Fellow of both the American Association for Artificial In
telligence and the ACM and is a member of the National Acade
my of Engineering.
DTSTART;TZID=Europe/Paris:20101026T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201010261
100
UID:LSVsemLSV.201010261100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Vérification des propriétés logiques avec des étiquettes
STATUS:CONFIRMED
ATTENDEE;CN="Mamadou Kanté
":
MAILTO:no@spam.com
DESCRIPTION:
Un système d'étiquetage pour une propriété P dans une struct
ure consiste à assigner à chaque élément du domaine une étiq
uette\, aussi petite que possible\, de telle sorte que l'on
puisse vérifier la propriété en ne regardant que les étiquet
tes. Les systèmes d'étiquetage peuvent Ãªtre vus comme un pr
é-traitement en vu de faire du model checking. En model-chec
king les objets manipulés sont le plus souvent statiques. Lo
rsque la structure est modifiée dans le temps\, on refait to
us les calculs. Nous nous intéressons aux structures qui peu
vent perdre des sommets/relations. Nous voulons pouvoir répo
ndre\, de manière rapide à n'importe quel moment\, si le gra
phe résultant après suppression de sommets/arÃªtes vérifie u
ne propriété P. Notre technique consiste à utiliser les syst
èmes d'étiquetage. Je montrerai comment vérifier des proprié
tés du premier ordre dans certaines classes de graphes en ut
ilisant des étiquettes de taille logarithmique (les étiquett
es sont calculées une seule fois). Un ingrédient principal e
st le résultat de Gaifman et une décomposition des formules
locales de Frick. Ces résultats peuvent Ãªtre étendus au com
ptage.
DTSTART;TZID=Europe/Paris:20100202T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201002021
100
UID:LSVsemLSV.201002021100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Computational Complexity of Constraint Satisfaction Problems
STATUS:CONFIRMED
ATTENDEE;CN="Manuel Bodirsky
":
MAILTO:no@spam.com
DESCRIPTION:
This talk is an introduction to techniques to determine the
computational complexity of constraint satisfaction problems
. The central concept here is the notion of a *polymorphism*
of a set of constraints. Polymorphisms can be used to trans
late questions about computational complexity into questions
of fundamental importance in universal algebra. I will firs
t give an overview over recent breakthrough results on const
raint satisfaction over finite domains based on this transla
tion. Then I give an introduction on how to generalize those
techniques from finite to infinite domain constraint satisf
action\, and present applications in temporal reasoning.
DTSTART;TZID=Europe/Paris:20100216T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=201002161
100
UID:LSVsemLSV.201002161100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
The Complexity of Nash Equilibria in Stochastic Games
STATUS:CONFIRMED
ATTENDEE;CN="Michael Ummels
":
MAILTO:no@spam.com
DESCRIPTION:
We analyse the computational complexity of finding Nash equi
libria in simple stochastic multiplayer games. We show that
restricting the search space to equilibria whose payoffs fal
l into a certain interval may lead to undecidability. In par
ticular\, we prove that the following problem is undecidable
: Given a game G\, does there exist a pure-strategy Nash equ
ilibrium of G where player 0 wins with probability 1. Moreov
er\, this problem remains undecidable if it is restricted to
strategies with (unbounded) finite memory. However\, if mix
ed strategies are allowed\, decidability remains an open pro
blem. One way to obtain a provably decidable variant of the
problem is restricting the strategies to be positional or st
ationary. For the complexity of these two problems\, we obta
in a common lower bound of NP and upper bounds of NP and PSP
ACE respectively.
DTSTART;TZID=Europe/Paris:20091208T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200912081
100
UID:LSVsemLSV.200912081100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Towards provable security against side-channel attacks
STATUS:CONFIRMED
ATTENDEE;CN="Boris KÃ¶pf
":
MAILTO:no@spam.com
DESCRIPTION:
Side-channel attacks threaten the security of cryptographic
algorithms by exploiting information that is revealed by the
physical characteristics of the algorithm's execution\, for
example through variations in the running time or power con
sumption. In distributed environments such as the Internet\,
timing attacks are the most daunting kind of side-channel a
ttack: Timing can be measured and exploited remotely\, openi
ng the door for a potentially large number of attackers. Unf
ortunately\, there have been no countermeasures against timi
ng attacks that are practical and provably secure at the sam
e time. In this talk\, I present work on novel methods for r
easoning about the security of countermeasures against side-
channel attacks. The basis for this work is a model that ena
bles one to express bounds for the amount of information tha
t can be extracted from a system in a side-channel attack. I
present algorithms for computing such bounds\, and I report
on experimental results where we apply these algorithms to
analyze concrete implementations of cryptographic algorithms
. One finding is that the state-of-the-art countermeasure ag
ainst timing attacks reduces the rate at which an implementa
tion leaks information about the key\, but that the entire k
ey information is still eventually revealed. Finally\, I pre
sent recent work where we propose a novel countermeasure aga
inst timing attacks that is provably secure in our model. A
case study shows that this countermeasure is also practical
in that it leads to implementations with minor performance o
verhead.
DTSTART;TZID=Europe/Paris:20091215T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200912151
100
UID:LSVsemLSV.200912151100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Time-Bounded Verification
STATUS:CONFIRMED
ATTENDEE;CN="Joel Ouaknine
":
MAILTO:no@spam.com
DESCRIPTION:
I will discuss some recent results on verification problems
for timed automata over time intervals of fixed\, bounded le
ngth.
DTSTART;TZID=Europe/Paris:20091027T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200910271
100
UID:LSVsemLSV.200910271100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Reachability in Parametric One-Counter Machines
STATUS:CONFIRMED
ATTENDEE;CN="James Worrell
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk we consider one-counter machines in which count
er updates can mention integer-valued parameters. Our main r
esult is to show NP-completeness of the problem of determini
ng whether a given state is reachable from the initial state
for some value of the parameters. Membership in NP is shown
by reduction to the existential fragment of Presburger arit
hmetic with divisibility.
DTSTART;TZID=Europe/Paris:20091103T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200911031
100
UID:LSVsemLSV.200911031100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Savez-vous compter ?
STATUS:CONFIRMED
ATTENDEE;CN="Julien Clément
":
MAILTO:no@spam.com
DESCRIPTION:
Les réseaux de capteurs mobiles font leur apparition en info
rmatique depuis plusieurs années. Les applications de ces ré
seaux sont nombreuses: environnementales\, militaires\, écon
omiques\, écologiques... Certaines caractéristiques de ces r
éseaux sont nouvelles et posent ainsi un défi pour les conce
pteurs d'algorithmes que nous sommes. Le modèle des protocol
es de population [AAD+04] a été conÃ§u pour représenter form
ellement les réseaux de capteurs constitués d'agents mobiles
dont la mémoire est très limitée\, sans aucun contrÃ´le sur
leur propre mouvement. Nous étendrons ce modèle en un modèl
e plus hétérogène dans lequel nous étudierons deux problèmes
particuliers. Dans cet exposé je présenterai en effet mes r
ésultats sur deux types d'algorithmes. Tout d'abord les 'alg
orithmes de comptage'\, permettant de compter le nombre d'ag
ents présents dans le système alors que des fautes peuvent s
urvenir. Puis\, nous étudierons un raffinement de ce modèle\
, afin de prendre en compte la différence de vitesse entre l
es agents\, dans lequel nous présenterons des 'algorithmes d
e collecte'\, permettant de rassembler les données mesurées
par les différents agents du réseau.
DTSTART;TZID=Europe/Paris:20091201T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200912011
100
UID:LSVsemLSV.200912011100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Finite Representations for Reconfigurable Systems
STATUS:CONFIRMED
ATTENDEE;CN="Roland Meyer
":
MAILTO:no@spam.com
DESCRIPTION:
To bridge the gap to existing automated verification techniq
ues\, we present finite representations for reconfigurable s
ystems (RS). Despite an unbounded number of components and c
onnections\, a large class of RS exhibits only finitely many
connection patterns at runtime; a property called structura
l stationarity. We propose a translation of structurally sta
tionary systems into finite place/transition Petri nets\, wh
ich allows us to reuse existing Petri net verification tools
for the verification of RS. To judge the expressiveness of
the system class\, we prove that structural stationarity is
equivalent to boundedness in the novel functions depth and b
readth. The breadth of a RS corresponds to the connection de
gree of the components\, while the depth measures their inte
rdependence. Investigating these larger classes\, we find th
at systems of bounded depth are well-structured. Therefore\,
properties can be decided on a finite prefix of the computa
tion tree. For systems of bounded breadth\, we show Turing c
ompleteness. To recover a Petri net translation for systems
of bounded depth\, we combine the newly developed structural
semantics with classical concurrency semantics. Although th
e resulting mixed translation generalises the previous appro
aches\, it does not cover the full class of depth bounded sy
stems. An undecidability proof for reachability shows that a
translation into finite nets does not exist for the full cl
ass.
DTSTART;TZID=Europe/Paris:20091124T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200911241
100
UID:LSVsemLSV.200911241100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Fragments of first-order logic over infinite words
STATUS:CONFIRMED
ATTENDEE;CN="Volker Diekert
":
MAILTO:no@spam.com
DESCRIPTION:
In my lecture I report about a joint work with Manfred Kufle
itner which was presented at STACS 09 in Freiburg. In that w
ork we give topological and algebraic characterizations as w
ell as language theoretic descriptions of the following subc
lasses of first-order logic for omega-languages: Sigma2\, FO
2\, the intersection of FO2 and Sigma2\, and Delta2 (and by
duality Pi2 and the intersection of FO2 and Pi2). These desc
riptions extend the respective results for finite words. In
particular\, we relate the above fragments to language class
es of certain (unambiguous) polynomials. The talk is interpl
ay of algebraic\, topological\, and language theoretic prope
rties.
DTSTART;TZID=Europe/Paris:20090929T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200909291
100
UID:LSVsemLSV.200909291100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Approximate Verification of Parameterized Systems
STATUS:CONFIRMED
ATTENDEE;CN="Giorgio Delzanno
":
MAILTO:no@spam.com
DESCRIPTION:
In the talk I will present a series of abstractions that can
be used to obtain approximated verification algorithms for
parameterized systems with global conditions and different t
ypes of topology (ordered/unordered arrays\, trees\, graphs)
. The verification algorithms perform a symbolic exploration
of a possibly infinite-state space and exploit the theory o
f well-quasi orderings for ensuring the theoretical terminat
ion of the analysis. The presentation is based on joint work
with Parosh Abdulla and Ahmed Rezine.
DTSTART;TZID=Europe/Paris:20090922T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200909221
100
UID:LSVsemLSV.200909221100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Regular fixed points\, non-deterministic cyclic proofs and f
inite automata
STATUS:CONFIRMED
ATTENDEE;CN="David Baelde
":
MAILTO:no@spam.com
DESCRIPTION:
We consider encoding finite automata as least fixed points i
n a proof-theoretical framework equipped with a general indu
ction scheme\, and study automata inclusion in that setting.
We provide a coinductive characterization of inclusion that
yields a natural bridge to proof-theory. This leads us to g
eneralize these observations to regular formulas\, obtaining
new insights about inductive theorem proving and cyclic pro
ofs in particular.
DTSTART;TZID=Europe/Paris:20090715T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200907151
100
UID:LSVsemLSV.200907151100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
XPath: expressive power and static analysis
STATUS:CONFIRMED
ATTENDEE;CN="Balder ten Cate
":
MAILTO:no@spam.com
DESCRIPTION:
XPath is a language for navigating in XML documents. It is p
art of the W3C standard XML querying and processing language
s XQuery and XSLT. From the perspective of logic\, XPath can
be understood as a variant of temporal logics on finite tre
es. In this talk\, I will discuss two aspects of XPath 1.0 a
nd 2.0 (as well as of some other variants of XPath proposed
in the literature): Expressivity and succinctness: Which pat
hs through XML documents can be described in XPath\, and how
succinctly? One way to answer this is by comparing XPath to
more well established and understood languages such as firs
t-order logic. Static analysis: What is the complexity of te
sting whether two XPath expressions are equivalent (always g
ive the same answer)? Can we find a complete set of equivale
nce-preserving rewrite rules (i.e.\, so that every two equiv
alent expressions can be rewritten to each other using these
rules)? Based on joint works with Maarten Marx\, with Carst
en Lutz\, and with Luc Segoufin.
DTSTART;TZID=Europe/Paris:20090707T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200907071
100
UID:LSVsemLSV.200907071100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Using ProVerif to Analyze Protocols with XOR and Diffie-Hell
man Exponentiation
STATUS:CONFIRMED
ATTENDEE;CN="Ralf Küsters
":
MAILTO:no@spam.com
DESCRIPTION:
ProVerif is one of the most successful tools for cryptograph
ic protocol analysis. However\, dealing with algebraic prope
rties of operators such as the exclusive OR (XOR) and Diffie
-Hellman exponentiation has been problematic. In this talk\,
I will present an approach which enables ProVerif\, and rel
ated tools\, to analyze a large class of protocols that empl
oy the XOR operator and Diffie-Hellman exponentiation. The c
ore of our approach is to reduce the derivation problem for
Horn theories modulo algebraic properties of XOR/Diffie-Hell
man exponentiation to a purely syntactical derivation proble
m for Horn theories. The latter problem can then be solved b
y tools such as ProVerif. Our reduction works for a large cl
ass of Horn theories\, allowing to model a wide range of int
ruder capabilities and protocols. We implemented our reducti
on and\, in combination with ProVerif\, applied it in the au
tomatic analysis of several state-of-the-art protocols that
use XOR or Diffie-Hellman exponentiation. This talk is based
on joint work with Tomasz Truderung\, published at CCS 2008
and CSF 2009.
DTSTART;TZID=Europe/Paris:20090629T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200906291
100
UID:LSVsemLSV.200906291100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Specifying Interacting Components with Coordinated Concurren
t Scenarios
STATUS:CONFIRMED
ATTENDEE;CN="Madhavan Mukund
":
MAILTO:no@spam.com
DESCRIPTION:
We introduce a visual notation for local specification of co
ncurrent components based on message sequence charts (MSCs).
Each component is a finite-state machine whose actions are
MSCs that specify its local view of the overall communicatio
n in the system. These local MSCs are composed into coherent
global scenarios using a separately specified set of transa
ctions. Intuitively\, each MSC represents a phase of interac
tion. We introduce a mechanism to overlap phases that allows
complex interactions to be specified without obscuring the
logical structure of the constituent scenarios. Our notation
combines the global view available in models such as high-l
evel message sequence charts (HMSCs) with the local\, asynch
ronous structure captured by message-passing automata (MPA).
In fact\, both HMSCs and MPAs can be captured as special ca
ses of our formalism. In this talk we focus on the syntax an
d formal semantics of our notation\, with examples that illu
strate why this approach is more natural for capturing real-
life specifications. We also describe an approach to use aut
omated tools to analyze systems specified using our notation
. This is joint work with Prakash Chandrasekaran.
DTSTART;TZID=Europe/Paris:20090609T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200906091
100
UID:LSVsemLSV.200906091100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Weak Time Petri Nets Strike Back!
STATUS:CONFIRMED
ATTENDEE;CN="Arnaud Sangnier
":
MAILTO:no@spam.com
DESCRIPTION:
We consider the model of Time Petri Nets where time is assoc
iated with transitions. Two semantics for time elapsing can
be considered: the strong one\, for which all transitions ar
e urgent\, and the weak one\, for which time can elapse arbi
trarily. It is well known that many verification problems su
ch as the marking reachability are undecidable with the stro
ng semantics. In this talk\, we focus on Time Petri Nets wit
h weak semantics equipped with three different memory polici
es for the firing of transitions. We prove that the reachabi
lity problem is decidable for the most common memory policy
(intermediate) and becomes undecidable otherwise. Moreover\,
we study the relative expressiveness of these memory polici
es and obtain partial and surprising results. This a joint w
ork with Pierre-Alain Reynier (LIF-Université Aix-Marseille)
DTSTART;TZID=Europe/Paris:20090519T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200905191
100
UID:LSVsemLSV.200905191100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
High-Level Programming for E-Cash
STATUS:CONFIRMED
ATTENDEE;CN="Pedro AdÃ£o
":
MAILTO:no@spam.com
DESCRIPTION:
E-cash protocols aim at providing robust abstractions for an
onymous payment protocols. Properties of interest include\,
for instance\, that users can spend coins anonymously\, that
users cannot forge coins\, and that a user should not spend
the same coin twice without being eventually caught. These
protocols involve sophisticated cryptographic constructions
such as blind signatures and commitment and proving their co
rrectness is a non-trivial task\, hence reasoning about e-ca
sh applications becomes an almost impossible task. Relying o
n recent work on optimistic value commitment [FGZN08]\, we p
ropose a calculus to reason about e-cash applications. Our c
alculus has a simple\, symbolic semantics; it can be used fo
r programming with e-cash and for reasoning on its propertie
s\, while shielding the programmer from its cryptographic im
plementation. We consider two variants of the symbolic seman
tics. An abstract semantics rules out any double spending (b
y design) while a more realistic\, intermediate semantics ac
counts for the possibility of double spending\, with reliabl
e detection. We first relate these two semantics\, and then
relate the intermediate semantics to the computational prope
rties of the underlying e-cash protocol. We show that our ca
lculus is a sound abstraction of the low-level e-cash protoc
ols\, that is\, all low-level behaviours can be mapped to an
high-level equivalent trace.
DTSTART;TZID=Europe/Paris:20090512T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200905121
100
UID:LSVsemLSV.200905121100@lsv.ens-cachan.fr
LOCATION:Salle Condorcet (Bâtiment d'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Automated Computational Verification for Cryptographic Proto
col Implementations
STATUS:CONFIRMED
ATTENDEE;CN="Eugen Zalinescu
":
MAILTO:no@spam.com
DESCRIPTION:
We automatically verify implementations of cryptographic pro
tocols programmed in ML. We develop a prototype compiler fro
m a subset of ML to CryptoVerif\, Blanchet's prover for comp
utational cryptography. Thus\, we obtain a first tool chain
that yields security guarantees for computational models tig
htly related to executable code. We show the soundness of th
e underlying translation for authentication and secrecy. To
this end\, we equip ML programs with a probabilistic semanti
cs\, and relate it to the probabilistic polynomial-time sema
ntics of CryptoVerif. We also review experimental (symbolic
and computational) results recently obtained for a reference
implementation of the TLS protocol. (This is joint work wit
h Karthik Bhargavan\, Ricardo Corin\, and Cédric Fournet.)
DTSTART;TZID=Europe/Paris:20090428T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904281
100
UID:LSVsemLSV.200904281100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Test à partir de spécifications logiques
STATUS:CONFIRMED
ATTENDEE;CN="Delphine Longuet
":
MAILTO:no@spam.com
DESCRIPTION:
Le test est l'une des méthodes les plus utilisées pour la va
lidation des syst-bèmes informatiques. Lorsque l'implantati
on du système -Aà tester n'est pas connue\, les tests sont
sélectionnés et construits à partir d'une spécification (for
melle) du syst-bème. Il existe principalement deux approche
s du test -Aà partir de spécifications formelles : les spéc
ifications logiques sont utilisées pour tester le comporteme
nt fonctionnel des syst-bèmes (les donn-Aées)\, tandis que
les syst-bèmes de transitions sont utilis-Aés pour tester
le comportement dynamique et réactifs des syst-bèmes (acti
ons et communications).-A Une théorie du test à partir de s
pécifications logiques a été définie dans les années 90\, fo
rmalisant le cadre de test ainsi que les différentes phases
du processus de test. Ces travaux proposent en particulier u
ne méthode de sélection de tests appelée dépliage pour des s
pécifications de forme restreinte dont les axiomes sont des
équations conditionnelles. L'idée de cette méthode est d'uti
liser des techniques de preuve afin de guider la sélection d
e tests. Le but est d'obtenir une couverture pertinente des
comportements du syst-bème.-A Je présenterai tout d'abord
cette formalisation du test\, en particulier le probl-bème
de l'existence d'un jeu de tests exhaustif\, puis la m-Aéth
ode de sélection de tests par dépliage. Je présenterai ensui
te deux aspects de mes travaux : - la généralisation de ce c
adre de test aux spécifications du premier ordre\, et en par
ticulier les résultats d'exhaustivité et de complétude de la
sélection par dépliage étendue à ces spécifications - l'ada
ptation de ce cadre\, ainsi que les résultats d'exhaustivité
et l'adaptation du dépliage\, à des spécifications modales
du premier ordre\, dans le but de proposer une nouvelle appr
oche de test pour les syst-bèmes r-Aéactifs.
DTSTART;TZID=Europe/Paris:20090427T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904271
100
UID:LSVsemLSV.200904271100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Qualitative Determinacy and Decidability of Stochastic Games
with Partial Observation
STATUS:CONFIRMED
ATTENDEE;CN="Hugo Gimbert
":
MAILTO:no@spam.com
DESCRIPTION:
(Joint work with Nathalie Bertrand and Blaise Genest.) We co
nsider the standard model of finite two-person zero-sum stoc
hastic games with signals. We are interested in the existenc
e of almost-surely winning or positively winning strategies\
, under reachability\, safety\, Büchi or co-Büchi winning ob
jectives. We prove two qualitative determinacy results. Firs
t\, in a reachability game either player 1 can achieve almos
t surely the reachability objective\, or player 2 can ensure
almost surely the complimentary safety objective\, or both
players have positively winning strategies. Second\, in a Bü
chi game if player 1 cannot achieve almost surely the Büchi
objective\, then player 2 can ensure positively the complime
ntary co-Büchi objective. We prove that players only need st
rategies with finite-memory\, whose sizes range from no memo
ry at all to doubly-exponential size\, with matching lower b
ounds. We provide fix-point algorithms to decide which playe
r has an almost surely winning or positive winning strategy
and compute the finite memory strategy. Complexity ranges fr
om EXPTIME to 2EXPTIME with matching lower bounds\, and bett
er complexity can be achieved for some special cases where o
ne of the players is better informed than her opponent.
DTSTART;TZID=Europe/Paris:20090421T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904211
100
UID:LSVsemLSV.200904211100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Kleene et Kozen en Coq
STATUS:CONFIRMED
ATTENDEE;CN="Damien Pous
":
MAILTO:no@spam.com
DESCRIPTION:
Formaliser des choses dans un assistant de preuve s'av-bère
souvent-A pénible\, de nombreuses étapes de raisonnement d
evant -bÃªtre explicit-Aées alors qu'elles sont d'habitude
laissées au relecteur scrupuleux. Ceci est en particulier v
rai lorsque l'on doit travailler sur des relations binaires
(réécriture\, réductions\, équivalences\, etc...)\, tr-bès
-A intuitives\, mais pas compl-bètement triviales.-A Lorsq
ue c'est possible\, une premi-bère astuce consiste -Aà con
sidérer les relations de fa-bÃ§on alg-Aébrique : en montan
t le niveau d'abstraction\, on facilite la formalisation de
certaines preuves. Une fois ce pas franchi\, on réalise que
les relations binaires sont un mod-bèle des-A alg-bèbres
de Kleene\, d-Aécidables par la théorie des automates finis
. Nous exposerons un travail en cours\, sur une formalisatio
n Coq des automates - via des matrices\, afin d'obtenir une
tactique de décision des alg-bèbres de-A Kleene\, par réfl
ection. Plus généralement\, nous exposerons les outils que n
ous développons pour raisonner sur ce genre de structures al
gébriques.
DTSTART;TZID=Europe/Paris:20090414T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904141
100
UID:LSVsemLSV.200904141100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Logics with Rank Operators
STATUS:CONFIRMED
ATTENDEE;CN="Anuj Dawar
":
MAILTO:no@spam.com
DESCRIPTION:
It is a long-standing open problem in descriptive complexity
theory whether there is a logic that expresses exactly the
polynomial-time decidable properties of unordered structures
. It has been known since the early 90s that fixed-point log
ic with counting (FPC) is not sufficient and there have been
several proposals for more expressive logics. Taking our in
spiration from recent results that show that natural linear-
algebraic operations are not definable in FPC\, we propose F
PR - an extension of fixed-point logic with an operator for
matrix rank. We show that this is strictly more expressive t
han FPC and can express the polynomial-time problems that ha
ve been shown to be inexpressible in FPC. We also show that
FO+R\, the extension of first-order logic with rank operator
s is surprisingle expressive. It can express some forms of t
ransitive closure and\, on ordered structures\, captures the
complexity classes ModpL. In this talk\, I will give the hi
story and general background to the question (assuming littl
e or no previous knowledge of descriptive complexity and fix
ed-point logics) and explain the context of the new results.
I will also point to several interesting open problems. (Jo
int work with Martin Grohe\, Bjarki Holm and Bastian Laubner
).
DTSTART;TZID=Europe/Paris:20090407T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904071
100
UID:LSVsemLSV.200904071100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Games of ordinal Length
STATUS:CONFIRMED
ATTENDEE;CN="Florian Horn
":
MAILTO:no@spam.com
DESCRIPTION:
We present an extension of the classical model of infinite t
wo-player games\, allowing plays with arbitrary ordinal leng
th. In addition to the usual ''successor transitions''\, our
arenas feature ''limit transitions'' which describe what ha
ppens after partial plays whose length is a limit ordinal. T
he play only stops when it reaches a final state\, which can
be winning for either of the players. We describe two solut
ions for such games. The first one uses a reduction to infin
ite Muller games\, and shows that the problem of the winner
is PSPACE-complete. The second one uses a special case of or
dinal games with ''priority'' transitions\, where the player
s have positional strategies. A LAR-like construction allows
us to derive the existence of finite-memory strategies in t
he general case.
DTSTART;TZID=Europe/Paris:20090406T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200904061
100
UID:LSVsemLSV.200904061100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Cryptographic protocols as Building Blocks: From the Man-in-
the-Middle attack to Compositional Symbolic Analysis.
STATUS:CONFIRMED
ATTENDEE;CN="Cas Cremers
":
MAILTO:no@spam.com
DESCRIPTION:
Despite using very coarse abstractions\, and making strong a
ssumptions on the environment\, the symbolic analysis of cry
ptographic protocols has proven very successful. By now\, ma
ny dimensions of the symbolic (Dolev-Yao) model have been ex
plored to some extent\, including compositionality propertie
s of protocols and the relation between symbolic correctness
proofs and computational proofs. One might expect that form
al approaches are ideally suited for building larger communi
cation infrastructures\, because of their high level of abst
raction. However\, in practice\, symbolic methods are only u
sed for analysis of existing protocols\, whereas protocol co
nstruction is performed at the detailed level of cryptograph
ic protocols. In this talk we cover some of the requirements
for using cryptographic protocols as components in symbolic
\, Dolev-Yao like\, analyses. In particular\, we discuss var
ious compositionality results\, and their relation to using
cryptographic protocols as building blocks. Finally\, we rev
isit the cryptographic requirements on real-world protocols
and show how they influence the compositionality problem\, a
nd conclude with a number of open problems.
DTSTART;TZID=Europe/Paris:20090331T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903311
100
UID:LSVsemLSV.200903311100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
What's decidable for Asynchronous Programs?
STATUS:CONFIRMED
ATTENDEE;CN="Pierre Ganty
":
MAILTO:no@spam.com
DESCRIPTION:
An asynchronous or ''event-driven'' program is one that cont
ains procedure calls which are not directly executed from th
e call site\, but stored and executed later by an external s
cheduler. By providing a low-overhead way to manage concurre
nt interactions\, asynchronous programs form the core of man
y server programs\, embedded systems\, and popular programmi
ng styles for the web (Ajax). Unfortunately\, such programs
can be hard to write and maintain as sequential control flow
needs to be split into several disjoint handlers. They are
a challenge for static analysis tools as they are infinite s
tate: both the program stack and the number of outstanding a
synchronous requests may be unbounded. We show that safety a
nd liveness properties can be checked effectively for the cl
ass of Boolean asynchronous programs\, thus enabling automat
ic static techniques to check for correctness or for errors.
DTSTART;TZID=Europe/Paris:20090330T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903301
100
UID:LSVsemLSV.200903301100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
TPTP\, TSTP\, CASC\, etc. - Automated Reasoning in Practice
STATUS:CONFIRMED
ATTENDEE;CN="Geoff Sutcliffe
":
MAILTO:no@spam.com
DESCRIPTION:
This talk gives an overview of the activities and products t
hat stem from the Thousands of Problems for Theorem Provers
(TPTP) problem library for Automated Theorem Proving (ATP) s
ystems. These include the TPTP itself\, the Thousands of Sol
utions from Theorem Provers (TSTP) solution library\, the TP
TP language\, the CADE ATP System Competition (CASC)\, tools
such as my semantic Derivation Verifier (GDV) and the Inter
active Derivation Viewer (IDV)\, meta-ATP systems such as th
e Smart Selective Competition Parallelism (SSCPA) system and
the Semantic Relevance Axiom Selection System (SRASS)\, onl
ine access to automated reasoning systems and tools through
the SystemOnTPTP web service\, and applications in various d
omains. Current work extending the TPTP to higher-order logi
c will be introduced.
DTSTART;TZID=Europe/Paris:20090317T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903171
100
UID:LSVsemLSV.200903171100@lsv.ens-cachan.fr
LOCATION:Salle Renaudeau (Bâtiment Laplace)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
On the Reachability Analysis of Acyclic Networks of Pushdown
Systems
STATUS:CONFIRMED
ATTENDEE;CN="Tayssir Touili
":
MAILTO:no@spam.com
DESCRIPTION:
We address the reachability problem in acyclic networks of p
ushdown systems. We consider communication based either on s
hared memory or on message passing through unbounded lossy c
hannels. We prove mainly that the reachability problem betwe
en recognizable sets of configurations (i.e.\, definable by
a finite union of products of finite-state automata) is deci
dable for such networks\, and that for lossy channel pushdow
n networks\, the channel language is effectively recognizabl
e. This fact holds although the set of reachable configurati
ons (including stack contents) for a network of depth (at le
ast) 2 is not rational in general (i.e.\, not definable by a
multi-tape finite automaton). Moreover\, we prove that for
a network of depth 1\, the reachability set is rational and
effectively constructible (under an additional condition on
the topology for lossy channel networks). This is a joint wo
rk with Mohamed Faouzi Atig and Ahmed Bouajjani.
DTSTART;TZID=Europe/Paris:20090310T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903101
100
UID:LSVsemLSV.200903101100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Context-bounded analysis of multithreaded Java programs
STATUS:CONFIRMED
ATTENDEE;CN="Stefan Schwoon
":
MAILTO:no@spam.com
DESCRIPTION:
The reachability problem is undecidable for programs with bo
th recursive procedures and multiple threads with shared mem
ory. One approach to resolve this problem is to use context-
bounded reachability\, i.e. to consider only those runs in w
hich the active thread changes at most k times\, where k is
fixed. However\, until recently\, context-bounded reachabili
ty has been only a theoretical possibility\, primarily becau
se of its prohibitive worst-case runtime. In the talk\, whic
h presents joint work with Dejvuth Suwimonteerabuth and Javi
er Esparza\, I will talk about an improvement that alleviate
s this problem. The approach has been implemented in the too
l jMoped.
DTSTART;TZID=Europe/Paris:20090304T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903041
100
UID:LSVsemLSV.200903041100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
A weighted mu-calculus on words
STATUS:CONFIRMED
ATTENDEE;CN="Ingmar Meinecke
":
MAILTO:no@spam.com
DESCRIPTION:
We define a weighted mu-calculus on finite and infinite word
s. Hereby\, the mu-calculus does not use conjunction and the
weights are taken from semirings satisfying certain complet
eness and continuity properties. For important semirings lik
e distributive complete lattices\, the tropical and the prob
abilistic semiring\, we show that the formulas of the conjun
ction-free weighted mu-calculus define exactly the class of
omega-rational formal power series.
DTSTART;TZID=Europe/Paris:20090303T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200903031
100
UID:LSVsemLSV.200903031100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
On Simulation-Based Probabilistic Model Checking of Mixed-An
alog Circuits
STATUS:CONFIRMED
ATTENDEE;CN="Axel Legay
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk\, we consider verifying properties of mixed-sig
nal circuits\, i.e.\, circuits for which there is an interac
tion between analog (continuous) and digital (discrete) valu
es. We use a simulation-based approach that consists of eval
uating the property on a representative subset of behaviors\
, generated by simulation\, and answering the question of wh
ether the circuit satisfies the property with a probability
greater than or equal to some value. We propose a logic adap
ted to the specification of properties of mixed-signal circu
its\, in the temporal domain as well as in the frequency dom
ain. We also demonstrate the applicability of the method on
different models of Δ-Σ modulators for which previous formal
verification attempts were too conservative and required ex
cessive computation time. With Alexandre Donzé and Edmund Cl
arke.
DTSTART;TZID=Europe/Paris:20090224T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200902241
100
UID:LSVsemLSV.200902241100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Verifying Functional Properties of Pointer Programs
STATUS:CONFIRMED
ATTENDEE;CN="Ewen Maclean
":
MAILTO:no@spam.com
DESCRIPTION:
Separation logic has been used successfully to verify safety
properties of programs which manipulate the heap. The Small
foot family of program analysers are capable of verifying sh
ape properties of pointer programs\, for example analysing t
he shape of inductive structures on the heap\, such as linke
d lists. I discuss an extension to this work which concerns
the automatic verification of functional properties of point
er programs. I will discuss the challenging parts of such ve
rifications which require creative input. The talk will be m
otivated by examples and possibly a working demo of some of
the early results.
DTSTART;TZID=Europe/Paris:20090217T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200902171
100
UID:LSVsemLSV.200902171100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Regular graphs: a perfect model for infinite state systems?
STATUS:CONFIRMED
ATTENDEE;CN="Christophe Morvan
":
MAILTO:no@spam.com
DESCRIPTION:
There are dozens of models for infinite state systems. Indee
d\, Turing machine\, cellular automata\, pushdown systems\,
Petri nets\, or process algebras are only major examples of
such systems. Most of these systems do not provide the simpl
icity and efficiency of finite state systems. Finite graphs\
, or finite state automata\, are the corner stone of compute
r science\, it is still a very active field of research with
countless applications. Infinite state systems lack that ki
nd of universal and simple framework. Graph grammars were in
itially used to produce infinite sets of graphs. But in the
early 90's\, Courcelle used deterministic graph grammars to
characterise a general class of infinite graphs: regular gra
phs. Recently Caucal built up a nice toolbox for studying re
gular graphs\, and with Hassen they provided an elegant exte
nsion of visibly pushdown automata\, which captures every de
terministic context-free language. In this talk we will pres
ent a survey on regular graphs\, including a discussion on t
he extensions of visibly pushdown automata. We will present\
, as well\, an ongoing work with Nathalie Bertrand aiming at
generalising probabilistic pushdown automata to this graph
grammar setting.
DTSTART;TZID=Europe/Paris:20090210T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200902101
100
UID:LSVsemLSV.200902101100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Parameter Synthesis for Probabilistic Timed Reachability
STATUS:CONFIRMED
ATTENDEE;CN="Joost-Pieter Katoen
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk\, we propose a technique to synthesize parametr
ic rate values in continuous-time Markov chains that ensure
the validity of time-bounded reachability properties. Rate e
xpressions over variables indicate the average speed of stat
e changes and are expressed using the polynomials over reals
. The key contribution is an algorithm that approximates the
set of parameter values for which the stochastic real-time
system guarantees the validity of bounded reachability prope
rties. This algorithm is based on discretizing parameter ran
ges together with a refinement technique. We will describe t
he algorithm\, analyze its time complexity\, and show its ap
plicability by deriving parameter constraints for a real-tim
e storage system with probabilistic error checking facilitie
s. (This is joint work with Tingting Han and Alexandre Merea
cre.)
DTSTART;TZID=Europe/Paris:20090113T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200901131
100
UID:LSVsemLSV.200901131100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Analyses de propriétés quantitatives de programmes
STATUS:CONFIRMED
ATTENDEE;CN="Laure Gonnord
":
MAILTO:no@spam.com
DESCRIPTION:
Dans cet exposé je présenterai mes travaux doctoraux et post
doctoraux qui se placent tous les deux dans le contexte d'an
alyse des propriétés quantitatives de programmes dans le but
de faire des logiciels embarqués sûrs. Dans ma thèse\, j'ai
étudié l'analyse des relations linéaires\, qui permet de dé
couvrir automatiquement\, en chaque point de contrÃ´le d'un
programme\, des systèmes de contraintes linéaires invariante
s sur les variables numériques. Les résultats de l'analyse s
ont utilisables en compilation\, en vérification de programm
es et en parallélisation. Après une introduction rapide à ce
tte méthode\, je montrerai plus spécifiquement comment la pr
écision des analyses peut Ãªtre améliorée grâce à la notion
d'accélération abstraite. Mes travaux postdoctoraux ont étud
ié d'autres types d'applications embarquées que sont les app
lications multimédia. Ces applications ne sont plus critique
s\, mais par contre on désire évaluer et garantir des propri
étés extra fonctionnelles\, comme la qualité de service. En
effet\, la resource allouée à un composant logiciel peut évo
luer\, et on aimerait garantir une certaine fluidité de l'ap
plication. Je présenterai mes travaux de formalisation des c
ontraintes de ressources au sein d'une architecture logiciel
le à composants\, Qinna\, ainsi que les mécanismes de mainte
nance de ces contraintes.
DTSTART;TZID=Europe/Paris:20090106T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200901061
100
UID:LSVsemLSV.200901061100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
The State of Inductive Theorem Proving for Software Verifica
tion
STATUS:CONFIRMED
ATTENDEE;CN="Lucas Dixon
":
MAILTO:no@spam.com
DESCRIPTION:
Functional correctness for non-trivial properties of softwar
e requires inductive proof. Sadly this is an undecidable pro
blem which typically requires frustrating amounts of user gu
idance. Fortunately\, this makes it a fascinating topic for
research; indeed\, a significant strand of research consider
s heuristic approaches to inductive theorem proving\, driven
by syntactic observations. Recently\, a type-theory based f
orm of synthesis\, combined with an upside-down twist on rew
riting\, has led to some exciting results. In this talk I wi
ll outline the state the field\, give my view of the key int
uitions for the emerging proof strategies\, and highlight th
e exciting challenges currently being considered.
DTSTART;TZID=Europe/Paris:20081216T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200812161
100
UID:LSVsemLSV.200812161100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Quantitative Languages: Decision Problems\, Expressive Power
\, and Closure Properties
STATUS:CONFIRMED
ATTENDEE;CN="Laurent Doyen
":
MAILTO:no@spam.com
DESCRIPTION:
Quantitative generalizations of classical languages\, which
assign to each word a real number instead of a boolean value
\, have applications in modeling resource-constrained comput
ation. We use weighted automata (finite automata with transi
tion weights) to define several natural classes of quantitat
ive languages over finite and infinite words; in particular\
, the real value of an infinite run is computed as the maxim
um\, limsup\, liminf\, limit average\, or discounted sum of
the transition weights. We define the classical decision pro
blems of automata theory (emptiness\, universality\, languag
e inclusion\, and language equivalence) in the quantitative
setting and study their computational complexity. As the dec
idability of language inclusion remains open for some classe
s of weighted automata\, we introduce a notion of quantitati
ve simulation that is decidable and implies language inclusi
on. We also give a complete characterization of the expressi
ve power of the various classes of weighted automata. In par
ticular\, we show that most classes of weighted automata can
not be determinized. Finally\, for quantitative languages L\
, L'\, we study the operations max(L\,L')\, min(L\,L')\, and
1-L as natural generalizations of the boolean operations; w
e also consider the sum L + L'. We establish the closure pro
perties of all classes of quantitative languages with respec
t to these four operations. This talk is based on joint work
with Krishnendu Chatterjee and Tom Henzinger.
DTSTART;TZID=Europe/Paris:20081215T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200812151
100
UID:LSVsemLSV.200812151100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
An Easy Algorithm For The General Vector Addition System Rea
chability Problem
STATUS:CONFIRMED
ATTENDEE;CN="JérÃ´me Leroux
":
MAILTO:no@spam.com
DESCRIPTION:
The reachability problem for Vector Addition Systems (VAS)
or equivalently for Petri Nets is a central problem of net t
heory. The general problem is known decidable by algorithms
exclusively based on the classical Kosaraju-Lambert-Mayr-Sac
erdote-Tenney (KLMST) decomposition. This decomposition is d
ifficult and it just has a non-primitive recursive upper-bou
nd complexity. In this paper\, we prove that if a final conf
iguration is not reachable from an initial one\, there exist
s a pair of Presburger formulas denoting an inductive separa
tor proving this property. Since we can decide with any deci
sion procedure for the Presburger arithmetic if pairs of Pre
sburger formulas denote inductive separators\, we deduce tha
t there exist checkable certificates of non-reachability. In
particular\, there exists an easy algorithm for deciding th
e general VAS reachability problem based on two semi-algorit
hms. A first one that tries to prove the reachability by fai
rly enumerating finite sequence of actions and a second one
that tries to prove the non-reachability by fairly enumerati
ng pairs of Presburger formulas. Even if the KLMST decomposi
tion is used for proving the termination\, this algorithm is
the very first one that can be implemented without using it
.
DTSTART;TZID=Europe/Paris:20081209T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200812091
100
UID:LSVsemLSV.200812091100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
XML Reasoning: From Theory to Practice
STATUS:CONFIRMED
ATTENDEE;CN="Pierre Genevès
":
MAILTO:no@spam.com
DESCRIPTION:
In the research for XML static type systems\, one challenge
is to deal with XPath powerful navigational features. I wil
l present a fixpoint modal logic designed for reasoning on f
inite trees\, along with a satisfiability-testing algorithm
that performs well in practice. The fully implemented system
allows to effectively solve a whole class of problems invol
ving XPath queries\, regular tree types and any boolean comb
ination of them (like query containment\, and query satisfia
bility in the presence of schemas).
DTSTART;TZID=Europe/Paris:20081125T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200811251
100
UID:LSVsemLSV.200811251100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
From Philosophical to Industrial Logics
STATUS:CONFIRMED
ATTENDEE;CN="Moshe Vardi
":
MAILTO:no@spam.com
DESCRIPTION:
One of the surprising developments in the area of program v
erification is how several ideas introduced by logicians in
the first part of the 20th century ended up yielding at the
start of the 21st century industry-standard property-specifi
cation languages called PSL and SVA. This development was en
abled by the equally unlikely transformation of the mathemat
ical machinery of automata on infinite words\, introduced in
the early 1960s for second-order arithmetics\, into effecti
ve algorithms for industrial model-checking tools. This talk
attempts to trace the tangled threads of this development.
DTSTART;TZID=Europe/Paris:20081106T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200811061
100
UID:LSVsemLSV.200811061100@lsv.ens-cachan.fr
LOCATION:Amphithéâtre Marie Curie (bâtiment d'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Questions de théorie des jeux et de convexité abstraite en a
nalyse statique de programme
STATUS:CONFIRMED
ATTENDEE;CN="Stéphane Gaubert
":
MAILTO:no@spam.com
DESCRIPTION:
Le but de cet exposé est de donner quelques exemples d'appli
cation de techniques d'optimisation et de théorie des jeux e
n analyse statique de programme par interprétation abstraite
. On présentera tout d'abord une correspondance entre les pr
oblèmes de point fixe rencontrés en interprétation abstraite
et ceux que l'on rencontre en théorie des jeux à somme null
e. Cette correspondance permet d'adapter des algorithmes ins
pirés de la théorie des jeux ou du contrÃ´le tels que l'itér
ation sur les politiques\, mais le caractère "expansif" des
opérateurs de point fixe\, qui se traduit par la présence d'
un taux d'actualisation négatif\, pose des difficultés algor
ithmiques inédites. On discutera notamment le problème du ca
lcul du point fixe minimal (ou de la vérification de la mini
malité d'un point fixe) à l'aide de techniques de théorie de
Perron-Frobenius non-linéaire. On montrera ensuite comment
des idées empruntées à l'analyse convexe abstraite permetten
t de définir des classes de domaines généralisant le domaine
des "templates" introduit par Manna et ses collaborateurs.
On traitera spécialement du domaine des polyèdres max-plus o
u tropicaux. Ces résultats sont issus de travaux en collabor
ation avec A. Adje (LIX/MeASI)\, X. Allamigeon (EADS)\, E. G
oubault et S. Putot (CEA/MeASI).
DTSTART;TZID=Europe/Paris:20081104T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200811041
100
UID:LSVsemLSV.200811041100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Tree Pattern Rewriting Systems
STATUS:CONFIRMED
ATTENDEE;CN="Olivier Serre
":
MAILTO:no@spam.com
DESCRIPTION:
Classical verification often uses abstraction when dealing w
ith data. On the other hand\, dynamic XML-based applications
have become pervasive\, for instance with the ever growing
importance of web services. We define here Tree Pattern Rewr
iting Systems (TPRS) as an abstract model of dynamic XML-bas
ed documents. TPRS systems generate infinite transition syst
ems\, where states are unranked and unordered trees (hence p
ossibly modeling XML documents). The guarded transition rule
s are described by means of tree patterns. Our main result i
s that given a TPRS system (T\,R)\, a tree pattern P and som
e integer k such that any reachable document from T has dept
h at most k\, it is decidable (albeit of non elementary comp
lexity) whether some tree satisfying P is reachable from T.
This is joint work with B. Genest\, A. Muscholl\, and M. Zei
toun.
DTSTART;TZID=Europe/Paris:20081028T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200810281
100
UID:LSVsemLSV.200810281100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Génération Automatique d'Approximations Régulières
STATUS:CONFIRMED
ATTENDEE;CN="Pierre-Cyrille Héam
":
MAILTO:no@spam.com
DESCRIPTION:
Etant donnés deux langages réguliers d'arbres I et B\, et u
n système de réécriture R\, on ne peut pas décider si R*(I)
et B ont une intersection vide\, m-bÃªme pour des syst-Aèm
es de réécritures simples. Une approche pour résoudre ce pro
blème consiste alors à utiliser des approximations de R*(I).
Nous montrerons dans cet exposé comment une technique manue
lle d'approximations introduite par Th. Genet en 98 peut -b
Ãªtre automatis-Aée\, notamment pour la vérification de pro
tocoles cryptographiques.
DTSTART;TZID=Europe/Paris:20081014T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200810141
100
UID:LSVsemLSV.200810141100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Diagnostic et Test en ordres partiels
STATUS:CONFIRMED
ATTENDEE;CN="Stefan Haar
":
MAILTO:no@spam.com
DESCRIPTION:
The talk takes a stand to advocate the use of partial order
unfolding semantics for the analysis of large networked sys
tems\, exemplified by fault diagnosis in telecommunication n
etworks. The methodology of asynchronous diagnosis is presen
ted\, followed by a discussion of fun but challenging proble
ms connected to diagnosis\, in particular distribution of un
folding. In a different domain\, the talk will present recen
t and ongoing work on testing of input/output automata over
partially ordered I/O streams.
DTSTART;TZID=Europe/Paris:20080930T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200809301
100
UID:LSVsemLSV.200809301100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Génération d'une suite de tests de grammaticalité
STATUS:CONFIRMED
ATTENDEE;CN="Sylvain Schmitz
":
MAILTO:no@spam.com
DESCRIPTION:
L'exposé s'intéresse à des techniques de fouille d'erreurs
dans une grammaire du fran-bÃ§ais d-Aéveloppée au LORIA. C
ette grammaire\, de taille importante\, utilisée à la fois p
our l'analyse syntaxique et la génération de texte\, souffre
de problèmes de sur-génération : elle décrit des phrases in
correctes. Pour un ensemble de phrases de test\, la fouille
d'erreurs cherche alors à identifier les causes les plus pro
bables de sur-génération pour assister le linguiste dans son
travail de correction. Je présenterai en détail une méthode
de génération de telles phrases qui vise à explorer les coi
ns et recoins de la grammaire et les interactions inattendue
s qu'elle permet.
DTSTART;TZID=Europe/Paris:20080923T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200809231
100
UID:LSVsemLSV.200809231100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Programming in Malbolge
STATUS:CONFIRMED
ATTENDEE;CN="Masahiko Sakai
":
MAILTO:no@spam.com
DESCRIPTION:
Malbolge is known as one of the most esoteric programming l
anguages\, in which programming is very difficult. The diffi
culty comes from (a) its restrictive instructions\, (b) inst
ruction-replacement after execution and (c) restriction for
loadable data. In this talk\, we solve these problems and sh
ows that general loop-programming is possible in this langua
ge.
DTSTART;TZID=Europe/Paris:20080916T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200809161
100
UID:LSVsemLSV.200809161100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Regular Model Checking using nondeterministic tree automata
STATUS:CONFIRMED
ATTENDEE;CN="Tomas Vojnar
":
MAILTO:no@spam.com
DESCRIPTION:
Abstract regular tree model checking (ARTMC) is a generic t
echnique for automated formal verification of various kinds
of infinite-state and parameterised systems\, including\, e.
g.\, parameterised protocols or programs manipulating dynami
c\, pointer-linked data structures. ARTMC is based on repres
enting infinite sets of configurations of the examined syste
ms by finite tree automata whose efficient manipulation is t
hus crucial for an overall efficiency of ARTMC. It turns out
that a significant bottleneck in dealing with finite tree a
utomata is the need to determinise them when checking inclus
ion or within the classical automata minimisation procedure.
In the talk\, we will present several recent works whose ai
m is to eliminate the need to determinise the automata being
handled in ARTMC. In particular\, we will present methods f
or an antichain-based inclusion checking on nondeterministic
tree automata and efficient methods for reducing the size o
f such automata based on various types of upward\, downward\
, and composed (bi)simulations. According to our experimenta
l results\, these techniques really very significantly impro
ve the performance of ARTMC. The talk is based on joint work
with Ahmed Bouajjani and Tayssir Touili from LIAFA\, Peter
Habermehl from LSV\, Parosh Aziz Abdulla and Lisa Kaati from
Uppsala\, and Lukas Holik from FIT BUT.
DTSTART;TZID=Europe/Paris:20080708T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200807081
100
UID:LSVsemLSV.200807081100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Tableau-based decision procedure for the logic of strategic
ability in multi-agent systems ATL
STATUS:CONFIRMED
ATTENDEE;CN="Valentin Goranko
":
MAILTO:no@spam.com
DESCRIPTION:
The Alternating-time Temporal Logic (ATL)\, introduced by A
lur\, Henzinger\, and Kupferman\, is a logic for reasoning a
bout strategic abilities of agents and coalitions in multi-a
gent systems\, in which one can express statements\, such as
: "The agent (or\, coalition of agents) A has a strategy suc
h that\, if A follows that strategy then\, no matter what ot
her agents do\, the objective $\phi$ will be achieved"\, the
re the objective is itself a formula of ATL prefixed by a te
mporal operator such as `nexttime'\, `until'\, or `always in
the future'. Testing satisfiability in ATL has been proved
decidable (ExpTime complete)\, by using alternating tree aut
omata and by small model property\, but both methods have so
me practical deficiencies and are not suitable for manual ap
plication. In this talk I will give a concise introduction t
o ATL and then will present a recently developed decision pr
ocedure for testing satisfiability in ATL based on sound\, c
omplete\, and terminating incremental tableaux. This decisio
n procedure runs in the theoretically prescribed time comple
xity\, i.e.\, ExpTime\, but in most practical cases is much
more efficient\, and is suitable for both manual and compute
rized application. (Joint work with Dmitry Shkatov\, Univ. o
f the Witwatersrand)
DTSTART;TZID=Europe/Paris:20080701T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200807011
100
UID:LSVsemLSV.200807011100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Star-height of tree languages
STATUS:CONFIRMED
ATTENDEE;CN="Christof LÃ¶ding
":
MAILTO:no@spam.com
DESCRIPTION:
The star-height problem for regular word languages is to de
termine for a given regular language the minimal number of n
estings of Kleene-stars required in a regular expression def
ining the given language. We consider the corresponding prob
lem for regular tree languages and show that this problem is
decidable. We do this by adapting a proof method that was u
sed by Daniel Kirsten to the setting of trees.
DTSTART;TZID=Europe/Paris:20080617T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200806171
100
UID:LSVsemLSV.200806171100@lsv.ens-cachan.fr
LOCATION:Amphi 109N (Bât. Léonard de Vinci)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Precise Fixpoint-Based Analysis of Programs with Thread-Crea
tion and Procedures
STATUS:CONFIRMED
ATTENDEE;CN="Markus Müller-Olm
":
MAILTO:no@spam.com
DESCRIPTION:
Most papers on precise analysis of parallel programs descri
be process creation by parbegin/parend blocks or their inter
procedural counterpart\, parallel procedure calls. In these
models\, the creator of processes running in parallel must w
ait until all the created processes have terminated before i
t can resume its execution. However\, in presence of procedu
res or methods\, this does not allow one to model thread cre
ation primitives as the found in languages like Java adequat
ely. In this talk I am going to present recent work on fixpo
int-based analysis of programs with thread creation and (rec
ursive) procedures. Our algorithm solves gen/kill-problems p
recisely up to abstraction of synchronization common in this
line of research; it can handle forward as well as backward
problems. Our results complement earlier work on automata-b
ased analysis of similar program models. The resulting algor
ithm\, however\, computes global information faster and more
directly. This is joint work with Peter Lammich.
DTSTART;TZID=Europe/Paris:20080603T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200806031
100
UID:LSVsemLSV.200806031100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Accelerated Data-flow Analysis
STATUS:CONFIRMED
ATTENDEE;CN="Grégoire Sutre
":
MAILTO:no@spam.com
DESCRIPTION:
Acceleration in symbolic verification consists in computing
the exact effect of some control-flow loops in order to spe
ed up the iterative fix-point computation of reachable state
s. Even if no termination guarantee is provided in theory\,
successful results were obtained in practice by different to
ols implementing this framework. In this talk\, we show how
to extend the acceleration framework to data-flow analysis.
Compared to a classical widening/narrowing-based abstract in
terpretation\, the loss of precision is controlled here by t
he choice of the abstract domain and does not depend on the
way the abstract value is computed. We illustrate our approa
ch on convex polyhedral data-flow analysis\, and we provide
a cubic-time acceleration-based algorithm for solving interv
al constraints with full multiplication. Joint work with Jér
Ã´me Leroux.
DTSTART;TZID=Europe/Paris:20080527T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200805271
100
UID:LSVsemLSV.200805271100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Systèmes dynamiques linéaires : décidabilité de problèmes de
sécurité
STATUS:CONFIRMED
ATTENDEE;CN="Emmanuel Hainry
":
MAILTO:no@spam.com
DESCRIPTION:
Les systèmes dynamiques décrivent un processus (trajectoire
\, phénomène naturel\, calcul) par l'espace sur lequel il se
produit\, sa dynamique et son point initial. Cette descript
ion est suffisante pour définir toute l'évolution du système
mais ne donne guère d'idée sur l'ensemble de la trajectoire
du système\, et il est crucial pour certains systèmes d'ass
urer des propriétés sur cette trajectoire (par exemple\, la
comète repassera infiniment souvent par un point donné\, ou
la Terre et la Lune ne se heurteront jamais ou encore la mac
hine de Turing s'arr-bÃªte).-A Nous définirons quelques pr
oblèmes importants sur les systèmes linéaires : atteignabili
té point à point\, atteignabilité d'un hyperplan\, omega-lim
ite. Nous montrerons que ces problèmes qui sont dans le cas
général (et m-bÃªme dans des cas simples) ind-Aécidables d
eviennent décidables si l'on considère des systèmes dynamiqu
es linéaires.
DTSTART;TZID=Europe/Paris:20080520T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200805201
100
UID:LSVsemLSV.200805201100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
&AGRAVE; la recherche de méthodes efficaces pour la vérifica
tion de réseaux de Petri à chronomètres en temps discret
STATUS:CONFIRMED
ATTENDEE;CN="Morgan Magnin
":
MAILTO:no@spam.com
DESCRIPTION:
A mesure que les réseaux proliféraient et prenaient une pla
ce temporelle et fonctionnelle des systèmes. Il convient ain
si de développer des formalismes permettant d'écrire et de v
alider les interactions entre les activités des processeurs
et les réseaux de communication. Les réseaux de Petri tempor
els (RdPT) sont un de ces formalismes. Ils permettent de mod
éliser la durée de différentes actions sous la forme d'un in
tervalle de temps. Ils peuvent par ailleurs -bÃªtre enrichi
s afin de repr-Aésenter des tâches susceptibles d'-bÃªtre
suspendues puis relanc-Aées (réseaux de Petri à chronomètre
s notés SwPN). Le temps dense consiste à considérer le temps
comme une grandeur dense tandis que le temps discret l'assi
mile à une grandeur discrète. Les applications physiques évo
luent par rapport au temps physique qui est continu ; toutef
ois\, l'évolution du procédé n'est en général observée par l
e système informatique qui ne le pilote qu'à des instants pa
rticuliers (échantillonnage ou observations sporadiques). De
plus\, le système de pilotage est composé de tâches qui son
t exécutées sur un (ou plusieurs) processeur(s) dont le temp
s physique est discret. Le recours à un temps dense lors de
la modélisation conduit donc à une surapproximation du systè
me informatique. Mais l'intér-bÃªt majeur du temps dense r
-Aéside dans les abstractions symboliques associées\, pratiq
ues à mettre en oeuvre et contenant l'explosion combinatoire
des états. Nous nous proposons de comparer les deux approch
es que sont le temps dense et le temps discret. Notre étude
commence par un approfondissement des liens entre réseaux de
Petri\, RdPT et SwPN en fonction de leur sémantique en temp
s dense et en temps discret. Nous en déduisons des résultats
de décidabilité importants sur les modèles en temps discret
\, notamment la décidabilité de l'accessibilité d'état sur l
es SwPN bornés. Nous proposons ensuite une méthode efficace
de calcul énumératif de l'espace d'états de modèles en temps
discret. Comme toute méthode purement énumérative\, celle-c
i souffre toutefois de l'explosion combinatoire du nombre d'
états. C'est pourquoi nous concevons une méthode symbolique
permettant de calculer l'espace d'états d'un modèle en temps
discret en adaptant les techniques habituellement réservées
au temps dense. Cette procédure nous permet alors de vérifi
er des propriétés exprimées dans la logique TCTL sur les SwP
N en temps discret. Nous aboutissons à des résultats très en
courageants\, qui permettent d'analyser finement le comporte
ment de modèles à chronomètres.
DTSTART;TZID=Europe/Paris:20080513T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200805131
100
UID:LSVsemLSV.200805131100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
On the use of formal models for proving cryptographic securi
ty notions
STATUS:CONFIRMED
ATTENDEE;CN="Véronique Cortier
":
MAILTO:no@spam.com
DESCRIPTION:
Since the 1980s\, two approaches have been developed for an
alyzing security protocols. One of the approaches relies on
a computational model that considers issues of complexity an
d probability. This approach captures a strong notion of sec
urity\, guaranteed against all probabilistic polynomial-time
attacks. The other approach relies on a symbolic model of p
rotocol executions in which cryptographic primitives are tre
ated as black boxes. Since the seminal work of Dolev and Yao
\, it has been realized that this latter approach enables si
gnificantly simpler and often automated proofs. However\, th
e guarantees that it offers have been quite unclear. In this
talk\, we present several approaches that enable to obtain
the best of both worlds: fully automated proofs and strong\,
clear security guarantees.
DTSTART;TZID=Europe/Paris:20080506T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200805061
100
UID:LSVsemLSV.200805061100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Conflict-Tolerant Real-Time Features
STATUS:CONFIRMED
ATTENDEE;CN="Deepak D'Souza
":
MAILTO:no@spam.com
DESCRIPTION:
This work addresses the problem of detecting and resolving
conflicts due to timing constraints imposed by features in r
eal-time systems. We consider systems composed of a base sys
tem with multiple "features" or "controllers"\, each of whic
h independently advises the system on how to react to input
events so as to conform to their individual specifications.
We propose a methodology for developing such systems in a mo
dular manner based on the notion of "conflict-tolerant" feat
ures that are designed to continue offering advice even when
their advice has been overridden in the past. We give a sim
ple priority-based scheme for composing such features\, whic
h guarantees the "maximal" use of each feature. We provide a
formal framework for specifying such features\, and a compo
sitional technique for verifying systems developed in this f
ramework. This is joint work with Madhu Gopinathan\, Prahlad
Sampath\, and S. Ramesh.
DTSTART;TZID=Europe/Paris:20080429T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200804291
100
UID:LSVsemLSV.200804291100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Data Tree Patterns
STATUS:CONFIRMED
ATTENDEE;CN="Claire David
":
MAILTO:no@spam.com
DESCRIPTION:
One difficulty when we want to specify and manipulate XML d
ocuments is to deal with data. Here we represent an XML docu
ment as a tree labelled by an infinite alphabet to represent
data values. We consider Boolean combinations of data tree
patterns as a specification and query language for XML docum
ents. Data tree patterns are tree patterns plus variable (in
)equalities which express joins between data values. We cons
ider the decidability and complexity of two problems. The fi
rst one is the model checking problem. We show that it is DP
-complete in general and already NP-complete when we conside
r a single pattern. The second one is the satisfiability pro
blem in the presence of a DTD. We show that it is in general
undecidable and we identify several decidable fragments.
DTSTART;TZID=Europe/Paris:20080408T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200804081
100
UID:LSVsemLSV.200804081100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Data Exchange and Schema Mappings in Open and Closed Worlds
STATUS:CONFIRMED
ATTENDEE;CN="Cristina Sirangelo
":
MAILTO:no@spam.com
DESCRIPTION:
Data exchange is the problem of translating a source databa
se structured according to a source schema into a new databa
se structured according to a given target schema\, known the
relationship between the source and the target (schema mapp
ing). Two semantics of data exchange and schema mappings hav
e been proposed in the literature: an open-world (OWA) seman
tics \, which allows target instances to contain arbitrary e
xtensions of the data translated from the source\, a closed-
world (CWA) semantics\, which only allows to exchange "as mu
ch data as needed" to satisfy the constraints of the schema
mapping. This work proposes a new mixed OWA/CWA semantics th
at generalizes and unifies the previous ones: it allows diff
erent target attributes to import data according to differen
t semantics (either open-world or closed-world). This approa
ch allows more flexibility in the specification of schema ma
ppings and collapses in the known OWA and CWA approaches whe
n target attributes are either all open or all closed. Under
such mixed semantics\, we address two of the main issues in
data exchange and schema management: query answering and co
mposition of schema mappings. In particular we study how the
ir complexities depend on the number of open attributes and
we identify new conditions under which schema mappings compo
se.
DTSTART;TZID=Europe/Paris:20080401T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200804011
100
UID:LSVsemLSV.200804011100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Relational data types and proofs with Moca
STATUS:CONFIRMED
ATTENDEE;CN="Richard Bonichon
":
MAILTO:no@spam.com
DESCRIPTION:
A relational data type is a concrete data type that declare
s invariants or relations that are verified by its construct
ors (see [1]). Moca [2] is a generic construction function g
enerator for OCaml data types. It allows the definition of c
omplex invariants on data typs\, which are then automagicall
y managed. This talk will be divided into three parts: - I w
ill first introduce some theoretical background about relati
onal data types; - then I will show how one can specify and
use invariants with Moca; - I will end the talk with a discu
ssion about how one can apply such a tool in the context of
automated theorem proving. We will in particular evoke the c
ase of deduction modulo [3\, 4] and the zenon automated theo
rem prover [5\, 6]. [1] On the implementation of constructor
functions for non-free concrete data types. F. Blanqui\, T.
Hardin et P. Weis [2] Moca [3] Theorem proving modulo\, rev
ised version. G. Dowek\, Th. Hardin\, and C. Kirchner [4] Ta
MeD: a Tableaud Method for Deduction Modulo. R. Bonichon [5]
Zenon : An Extensible Automated Theorem Prover Producing Ch
eckable Proof. R. Bonichon\, D. Delahaye and D. Doligez [6]
Zenon
DTSTART;TZID=Europe/Paris:20080325T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200803251
100
UID:LSVsemLSV.200803251100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Extrapol : Extraction de politiques de sécurité depuis C
STATUS:CONFIRMED
ATTENDEE;CN="David Teller
":
MAILTO:no@spam.com
DESCRIPTION:
De nos jours\, les technologies les plus avancées disponibl
es pour garantir la sûreté d'un système Linux vis-à-vis de p
rocessus malicieux ou bogués sont SELinux\, AppArmor et quel
ques autres techniques comparables de pare-feux internes. Da
ns chacun des cas\, l'approche consiste à surveiller dynamiq
uement les interactions entre processus ou entre processus e
t objets du système et à interdire celles qui ne sont pas ex
plicitement autorisées par une "politique de sécurité". Si l
'idée est intéressante\, son implantation se révèle souvent
trop complexe pour la mise en oeuvre\, notamment en raison d
e la difficulté à valider une nouvelle politique de sécurité
sans devoir tester exhaustivement tous les logiciels instal
lés. C'est à ce point qu'entre en jeu l'analyse statique : c
omment\, à partir d'une politique de sécurité\, vérifier sta
tiquement la compatibilité avec les logiciels déjà installés
sur le système\, ou avec de nouveaux logiciels à installer
? C'est sur ce problème que nous travaillons dans le cadre d
'Extrapol : à partir du modèle de sécurité imposé par SELinu
x\, des systèmes de types à la Hindley-Milner et des types d
épendants\, nous définissons un mécanisme d'extraction de po
litiques de sécurité à partir de bibliothèques et de fonctio
ns écrites en langage C. Au cours de cet exposé\, nous prése
nterons le modèle de sécurité de SELinux\, la transformation
de ce modèle en un jeu de contraintes sur le langage C et l
e processus d'extraction.
DTSTART;TZID=Europe/Paris:20080318T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200803181
100
UID:LSVsemLSV.200803181100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Approximate Satisfiability and Equivalence
STATUS:CONFIRMED
ATTENDEE;CN="Michel de Rougemont
":
MAILTO:no@spam.com
DESCRIPTION:
We show how to approximate decision problems such as satisf
iability of a formula by a structure\, or Equivalence betwee
n two formulas\, such that we gain an exponential factor (or
more) in complexity. A typical case is to decide if two Non
-deterministic automata are equivalent: we decide the approx
imate version in polynomial time whereas the exact version i
s PSPACE complete. For Pushdown automata\, we decide the app
roximate version in exponential time whereas the exact versi
on is undecidable.
DTSTART;TZID=Europe/Paris:20080311T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200803111
100
UID:LSVsemLSV.200803111100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Objets d'interaction et réseaux différentiels
STATUS:CONFIRMED
ATTENDEE;CN="Damiano Mazza
":
MAILTO:no@spam.com
DESCRIPTION:
Nous commencerons par une introduction generale et le plus
possible auto-contenue aux reseaux d'interaction et leurs ex
tensions non-deterministes et concurrentes (reseaux multipor
t\, reseaux differentiels...). On presentera en suite des re
sultats plus specifiques\, notamment une definition categori
que de modele denotationnel des combinateurs d'interaction\,
basée sur la notion d'"objet d'interaction". On terminera e
n voyant comment cette notion peut etre appliquee aussi aux
reseaux d'interaction diffrentiels.
DTSTART;TZID=Europe/Paris:20080304T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200803041
100
UID:LSVsemLSV.200803041100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
WYSINWYX: What You See Is Not What You eXecute
STATUS:CONFIRMED
ATTENDEE;CN="Thomas Reps
":
MAILTO:no@spam.com
DESCRIPTION:
What You See Is Not What You eXecute: computers do not execu
te source-code programs; they execute machine-code programs
that are generated from source code. Not only can the WYSINW
YX phenomenon create a mismatch between what a programmer in
tends and what is actually executed by the processor\, it ca
n cause analyses that are performed on source code -- which
is the approach followed by most security-analysis tools --
to fail to detect bugs and security vulnerabilities. To addr
ess the WYSINWYX problem\, we have developed algorithms to r
ecover information from stripped executables about the memor
y-access operations that the program performs. These algorit
hms are used in the CodeSurfer/x86 tool to construct interme
diate representations that are used for browsing\, inspectin
g\, and analyzing stripped x86 executables. Recently\, this
infrastructure has been used to create a tool for looking fo
r bugs in stripped device-driver executables. Joint work wit
h G. Balakrishnan (UW)\, J. Lim (UW)\, and T. Teitelbaum (Co
rnell and GrammaTech\, Inc.).
DTSTART;TZID=Europe/Paris:20080219T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200802191
100
UID:LSVsemLSV.200802191100@lsv.ens-cachan.fr
LOCATION:Salle Condorcet (Bâtiment d'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
On decision problems for Probabilistic Büchi Automata
STATUS:CONFIRMED
ATTENDEE;CN="Nathalie Bertrand
":
MAILTO:no@spam.com
DESCRIPTION:
Probabilistic Büchi automata (PBA) are finite-state accepto
rs for infinite words where all choices are resolved by fixe
d distributions and where the accepted language is defined b
y the requirement that the measure of the accepting runs is
positive. In this work we describe a complementation operato
r for PBA and a discuss on several algorithmic problems for
PBA. All interesting problems\, such as checking emptiness o
r equivalence for PBA or checking whether a finite transitio
n system satisfies a PBA-specification\, turn out to be unde
cidable. An important consequence of these results are sever
al undecidability results for stochastic games with incomple
te information\, modelled by partially-observable Markov dec
ision processes (POMDP) and w-regular winning objectives. Fu
rthermore\, we study an alternative semantics for PBA where
it is required that almost all runs for an accepted word are
accepting\, which turns out to be less powerful\, but has a
decidable emptiness problem. This is a joint work with Chri
stel Baier and Marcus Groesser.
DTSTART;TZID=Europe/Paris:20080205T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200802051
100
UID:LSVsemLSV.200802051100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Unions of Type Interpretations
STATUS:CONFIRMED
ATTENDEE;CN="Colin Riba
":
MAILTO:no@spam.com
DESCRIPTION:
The most flexible strong normalization proofs methods for v
arious extensions of typed lambda-calculi use type interpret
ations. Among them we distinguish Girard's reducibility cand
idates\, Tait's saturated sets and interpretations based on
biorthogonality. In this talk we compare these different int
erpretations wrt their ability to handle rewriting and wrt t
heir stability by union. We first propose a generalization o
f the notion of neutral term in Girard's candidates that all
ows to define them in a generic way. Concerning stability by
union\, we recall that there are confluent typed rewrite sy
stems that do not admit stable by union type interpretations
. We present a necessary and sufficient condition for Girard
's candidate to be stable by union and a necessary and suffi
cient condition for the closure by union of biorthogonals to
be reduciblity candidates. The second condition is strictly
more general than the first one\, and allows to define Tait
's saturated sets for rewriting in a uniform way. Moreover\,
we show that for orthogonal constructor rewriting\, Girard'
s candidates are stable by union.
DTSTART;TZID=Europe/Paris:20080129T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200801291
100
UID:LSVsemLSV.200801291100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Automates et logiques pour les mots sur un alphabet infini
STATUS:CONFIRMED
ATTENDEE;CN="Alexis Bès
":
MAILTO:no@spam.com
DESCRIPTION:
Plusieurs modèles d'automates ont été proposés pour manipul
er des mots sur un alphabet infini. Ces mots apparaissent pa
r exemple dans l'étude de problèmes de vérification de systè
mes distribués ou temporisés\, ou encore de manipulation de
données semi-structurées. Un objectif commun est d'obtenir u
n modèle à la fois simple et expressif\, et qui conserve tan
t que possible les bonnes propriétés du modèle classique. Da
ns cet exposé on présentera un nouveau type d'automate dans
lequel l'alphabet A est vu comme le domaine d'une structure
M\, et les transitions de l'automate sont des formules du pr
emier ordre écrites dans le langage de M. Ce modèle s'inspir
e directement de la notion de puissance généralisée de struc
tures introduite par Feferman et Vaught à la fin des années
1950\, et généralise un modèle introduit récemment par Choff
rut et Grigorieff. On verra qu'il possède de bonnes propriét
és de clÃ´ture et de décision\, ainsi que plusieurs caractér
isations logiques. On présentera également une extension du
formalisme de Feferman et Vaught qui permet de pallier le ma
nque d'expressivité du modèle initial.
DTSTART;TZID=Europe/Paris:20080108T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200801081
100
UID:LSVsemLSV.200801081100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Equivalence of Labeled Markov Chains
STATUS:CONFIRMED
ATTENDEE;CN="Laurent Doyen
":
MAILTO:no@spam.com
DESCRIPTION:
We consider the equivalence problem for probabilistic machi
nes. Two probabilistic machines are equivalent if every fini
te sequence of observations has the same probability of occu
rrence in the two machines. We show that deciding equivalenc
e is polynomial for labeled Markov chains\, using a reductio
n to the equivalence problem for probabilistic automata\, wh
ich is known to be polynomial. We provide an alternative alg
orithm to solve the latter problem\, which is based on a new
definition of bisimulation for probabilistic machines. Then
\, we consider the equivalence problem for labeled Markov de
cision processes (LMDPs) which asks given two LMDPs whether
for every way of resolving the decisions in each of the proc
esses\, there exists a way of resolving the decisions in the
other process such that the resulting probabilistic machine
s are equivalent. The decidability of this problem remains o
pen. We show that the strategies used to resolve the decisio
ns can be restricted to be observation-based\, but may requi
re infinite memory. This is a joint work with Tom Henzinger
and Jean-Francois Raskin.
DTSTART;TZID=Europe/Paris:20071218T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200712181
100
UID:LSVsemLSV.200712181100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Ordinal recursive bounds for Higman's lemma
STATUS:CONFIRMED
ATTENDEE;CN="Adam Cichon
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk we give a constructive proof of Higman's lemma
for strings generated over a finite alphabet enabling us to
construct and characterise functions which bound the lengths
of bad sequences. These bounding functions are described by
ordinal-bÂrecursive definitions and their characterisatio
n is achieved with reference to known ordinal-recursive hier
archies of numberÂtheoretic functions.-A
DTSTART;TZID=Europe/Paris:20071204T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200712041
100
UID:LSVsemLSV.200712041100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Formal Analysis of Security APIs
STATUS:CONFIRMED
ATTENDEE;CN="Graham Steel
":
MAILTO:no@spam.com
DESCRIPTION:
Cash machines (ATMs) and other critical parts of the electr
onic payment infrastructure contain tamper-proof hardware se
curity modules (HSMs)\, which protect highly sensitive data
such as the keys used to obtain personal identification numb
ers (PINs). These HSMs have a restricted API that is designe
d to prevent malicious intruders from gaining access to the
data. However\, several attacks have been found on these API
s\, as the result of painstaking manual analysis by experts
such as Mike Bond and Jolyon Clulow. I have been carrying ou
t research aimed at formalising and mechanising the analysis
of these APIs. This talk will present some API attacks\, an
d some automated formal analysis using theorem provers\, pro
tocol analysis tools\, and the PRISM probabilistic model che
cker.
DTSTART;TZID=Europe/Paris:20071113T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200711131
100
UID:LSVsemLSV.200711131100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Integrating verification\, testing\, and learning for crypto
graphic protocols
STATUS:CONFIRMED
ATTENDEE;CN="Vlad Rusu
":
MAILTO:no@spam.com
DESCRIPTION:
Joint work with Martijn Oostdijk (Riscure\, NL)\, Jan Tretma
ns (EmbeddedSystems Institute\, NL)\, Rene de Vries (Radboud
University Nijmegen\, NL)and T. Willemse (Eindhoven Univers
ity of Technology\, NL) The verification of cryptographic pr
otocol specifications is an activeresearch topic and has rec
eived much attention from the formalverification community.
By contrast\, the testing of actual black-boximplementations
of protocols\, which is\, arguably\, as important asverific
ation for ensuring the correct functioning of protocols in t
he "real" world\, is little studied. We propose an approach
for checkingsecrecy and authenticity properties not only on
protocol specifications\,but also on black-box implementatio
ns. The approach is compositional andintegrates ideas from v
erification\, black-box testing\, and learning. Itis illustr
ated on the Basic Access Control protocol implemented inbiom
etric passports.
DTSTART;TZID=Europe/Paris:20071109T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200711091
100
UID:LSVsemLSV.200711091100@lsv.ens-cachan.fr
LOCATION:Amphi 112 (Bât. d'Alembert\, couloir du LPQM)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Making Random Choices Invisible to the Scheduler
STATUS:CONFIRMED
ATTENDEE;CN="Kostas Chatzikokolakis
":
MAILTO:no@spam.com
DESCRIPTION:
When dealing with process calculi and automata which express
both nondeterministic and probabilistic behavior\, it is cu
stomary to introduce the notion of scheduler to resolve the
nondeterminism. It has been observed that for certain applic
ations\, notably those in security\, the scheduler needs to
be restricted so not to reveal the outcome of the protocol's
random choices\, or otherwise the model of adversary would
be too strong even for "obviously correct" protocols. In thi
s talk I present a process-algebraic framework in which the
control on the scheduler can be specified in syntactic terms
\, and I show how to apply it to solve the problem mentioned
above. I also consider the definition of (probabilistic) ma
y and must preorders\, and show that they are precongruences
with respect to the restricted schedulers. Furthermore\, I
show that all the operators of the language\, except replica
tion\, distribute over probabilistic summation\, which is a
useful property for verification. This framework is applied
to the dining cryptographers problem\, where the scheduler p
roblem comes into play.
DTSTART;TZID=Europe/Paris:20071030T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200710301
100
UID:LSVsemLSV.200710301100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Decidability Results for Well-Structured Transition Systems
with Auxiliary Storage
STATUS:CONFIRMED
ATTENDEE;CN="Rohit Chadha
":
MAILTO:no@spam.com
DESCRIPTION:
We consider the problem of verifying the safety of well-uctu
red transition systems (WSTS) with auxiliary storage. WSTSs
with storage are automata that have (possibly) infinitely ma
ny control states along with an auxiliary store\, but which
have a well-quasi-ordering on the set of control states. The
set of reachable configurations of the tomaton may themselv
es not be well-quasi-ordered because of the presence of the
extra store. consider the coverability problem for such syst
ems\, which asks if it is possible to reach a ntrol state (w
ith some store value) that covers some given control state.
Our main result that if control state reachability is decida
ble for automata with some store and finitely control states
then the coverability problem can be decided for WSTSs (wit
h infinitely many ntrol states) and the same store\, provide
d the ordering on the control states has some special proper
ty. The special property we require is defined in terms of t
he existence of a ranking ction compatible with the transiti
on relation. We then show that there are several classes of
nfinite state systems that can be viewed as WSTSs with an au
xiliary storage. These can then be used to both reestablish
old decidability results\, as well as discover new ones.Join
t work with Mahesh Viswanathan.
DTSTART;TZID=Europe/Paris:20071023T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200710231
100
UID:LSVsemLSV.200710231100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Structured specification of strategies in games on graphs
STATUS:CONFIRMED
ATTENDEE;CN="R. Ramanujam
":
MAILTO:no@spam.com
DESCRIPTION:
The analysis of non-zero-sum games proceeds by determining t
he response of players to opponents' strategies. However\, t
his requires each player to know what every other player wou
ld do in every possible situation\, which is quite unrealist
ic in large games. We look at situations where players const
ruct bounded memory strategies in a structured manner\, wher
e the opponent's strategy may be known only by its propertie
s. In the new setting we study the algorithmic question of f
inding best response for a player. We also present a simple
modal logic to reason about strategies and show that checkin
g assertion on a game graph is decidable.
DTSTART;TZID=Europe/Paris:20070921T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200709211
100
UID:LSVsemLSV.200709211100@lsv.ens-cachan.fr
LOCATION:Salle Condorcet (Bât. d'Alembert)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Automatic Generation of Loop Invariants
STATUS:CONFIRMED
ATTENDEE;CN="Deepak Kapur
":
MAILTO:no@spam.com
DESCRIPTION:
An overview of the recent work in our group on automatic gen
eration of loop invariants using different approaches will b
e presented. Particularly\, a heuristic based on quantifier-
elimination will be reviewed. Methods based on abstract inte
rpretation and ideal-theoretic semantics of programming lang
uage constructs will be discussed. An approach based on solv
ing recurrences will be presented. These methods have been i
mplemented and successfully tried on many programs implement
ing nontrivial number theoretic functions. Some preliminary
ideas about how to generalize these approaches to work on da
ta types other than numbers will be discussed.
DTSTART;TZID=Europe/Paris:20070703T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200707031
100
UID:LSVsemLSV.200707031100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Formal Verification of Security Protocols using Automata
STATUS:CONFIRMED
ATTENDEE;CN="Roberto Segala
":
MAILTO:no@spam.com
DESCRIPTION:
In this talk we will show how it is possible to use Probabil
istic Automata for the verification of security protocols\,
and in particular how simulation-based proofs can be employe
d. The simulation method is useful in general to reduce the
analysis of global properties to the analysis of local prope
rties of single computational steps. We extend the same idea
to analyze global security properties. Since security holds
under computational assumptions and up to a negligible prob
ability of error\, we propose a notion of polynomially accur
ate simulation relation for Probabilistic Automata and we il
lustrate it by analyzing a simple authentication protocol. I
n particular we show how the negation of the step condition
of our simulation relation becomes the definition of a forge
r for a signature scheme.
DTSTART;TZID=Europe/Paris:20070619T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200706191
100
UID:LSVsemLSV.200706191100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Automatic Analysis of LAN Infrastructures
STATUS:CONFIRMED
ATTENDEE;CN="Christoph Weidenbach
":
MAILTO:no@spam.com
DESCRIPTION:
Important guarantees for LAN infrastructures include connect
ivity\, error detection/recovery\, robust changes and securi
ty. In the talk I will develop a LAN infrastructure model in
first-order logic enabling automatic analysis of such prope
rties. The model starts at the ethernet layer of the TCP/IP
stack and ranges up to application protocols such as DHCP.
DTSTART;TZID=Europe/Paris:20070614T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200706141
100
UID:LSVsemLSV.200706141100@lsv.ens-cachan.fr
LOCATION:Amphi 109 N (bât L. de Vinci)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Local Testing of Message Sequence Charts is Difficult
STATUS:CONFIRMED
ATTENDEE;CN="K. Narayan Kumar
":
MAILTO:no@spam.com
DESCRIPTION:
Message sequence charts are an attractive visual formalism u
sed to specify distributed communicating systems. One way to
test such a system is to substitute a component by a test p
rocess and observe its interaction with the rest of the syst
em. We consider the question of whether we can characterize
the distributed behaviour of such a system based on local ob
servations. The main difficulty is that local observations c
an combine in unexpected ways to define implied scenarios no
t present in the original specification. We consider variant
s of this simple notion of testing. In most cases the proble
m turns out to be undecidable. (Joint work with Puneet Bhate
ja\, Paul Gastin and Madhavan Mukund)
DTSTART;TZID=Europe/Paris:20070529T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200705291
100
UID:LSVsemLSV.200705291100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
BEGIN:VEVENT
SUMMARY:
Local Testing of Message Sequence Charts is Difficult
STATUS:CONFIRMED
ATTENDEE;CN="Madhavan Mukund
":
MAILTO:no@spam.com
DESCRIPTION:
We consider message sequence charts enriched with timing con
straints between pairs of events. As in the untimed setting\
, an infinite family of time-constrained message sequence ch
arts (TC-MSCs) is generated using an HMSC?a finite-state aut
omaton whose nodes are labelled by TC-MSCs. A timed MSC is a
n MSC in which each event is assigned an explicit time-stamp
. A timed MSC covers a TC-MSC if it satisfies all the time c
onstraints of the TC-MSC. A natural recognizer for timed MSC
s is a message-passing automaton (MPA) augmented with clocks
. The question we address is the following: given a timed sy
stem specified as a time-constrained HMSC H and an implement
ation in the form of a timed MPA A\, is every TC-MSC generat
ed by H covered by some timed MSC recognized by A? We give a
complete solution for locally synchronized time-constrained
HMSCs\, whose underlying behaviour is always regular. We al
so describe a restricted solution for the general case. This
is joint work with S Akshay and K Narayan Kumar.
DTSTART;TZID=Europe/Paris:20070522T110000
DURATION:PT1H
URL;VALUE=URI:http://www.lsv.ens-cachan.fr/Seminaires/?sem=200705221
100
UID:LSVsemLSV.200705221100@lsv.ens-cachan.fr
LOCATION:Salle de Conférence (Pavillon des Jardins)
END:VEVENT
END:VCALENDAR