LaBRI, Bordeaux
Le séminaire M2F a lieu en salle 178 un mardi sur deux à 14H.
Pour proposer un séminaire, le calendrier ci-dessous vous aidera à choisir une date disponible.
Pour s'abonner ou se désabonner de la liste de diffusion.
Pour s'inscrire au calendrier de l'équipe M2F.
Tous les exposés sont retransmis en ligne.
Date | Exposé de | Titre | Exposé en présence / virtuel |
---|---|---|---|
jeudi 28 mars à 13h | Jean-Marc Talbot | Reasoning about Quality in Hyperproperties | en présence |
Security properties such as non-interference cannot be expressed as properties of individual traces of a system. Therefore, the notion of hyperproperties has been introduced to overcome this limitation: a hyperproperty can express properties about pairs or more generally, sets of traces. An extension of the LTL logic (hyperLTL) has been proposed to define hyperproperties and some positive results such as decidability for the model-checking problem have been proven. Motivated by verifying quantitative security properties, we propose extensions of HyperLTL following the proposal of similar extensions of LTL by Almagor et al., namely LTL[F] for quantitative operators and LTL[D] for discounting temporal operators. Such extensions aim to quantify on how much a formula is satisfied by a system. We will present some algorithms for model-checking those logics. | |||
mardi 9 avril | Arnaud Durand | Enumeration Classes Defined by Circuits | en présence |
We refine the complexity landscape for enumeration problems by introducing very low classes defined by using Boolean circuits as enumerators. We locate well-known enumeration problems, e.g., from graph theory, Gray code enumeration, and propositional satisfiability in our classes. In this way we obtain a framework to distinguish between the complexity of different problems known to be computable with polynomial delay, for which a formal way of comparison was not possible to this day. The approach offers a different measure of efficient enumeration such as the one defined using Constant Delay in the context of enumeration for query answering. This is joint work with Nadia Creignou and Heribert Vollmer. | |||
mardi 30 avril | Akshay S. | TBA | en présence |
TBA | |||
mardi 21 mai | Joost-Pieter Katoen | TBA | en ligne |
TBA |