________________________________
De : akheireddine <akheireddine(a)lrde.epita.fr>
Envoyé : mercredi 6 décembre 2023 10:45
À : Annonces du LRDE <annonce(a)lrde.epita.fr>
Objet : [Lrde] [Lrde Annonce] Soutenance de thèse de Anissa Kheireddine
Bonjour,
J'ai le plaisir de vous inviter à la soutenance de ma thèse intitulée :
"Contributions au Bounded model-checking basé sur SAT
La soutenance sera présentée en français.
Elle aura lieu le mardi 19 décembre 2023 à partir de 10h00 (heure de
Paris),
en Amphi 401, EPITA, 14-16 Rue Voltaire, 94270 Le Kremlin-Bicêtre.
Vous êtes cordialement invité au pot qui suivra.
Composition du jury:
Rapporteur: Vijay Ganesh, Professeur, GT, Georgia Institute of
Technology.
Rapporteur: Ahmed Bounekkar, Maître de Conférences, ERIC,
Université Claude Bernard Lyon 1.
Examinatrice: Laure Petrucci, Professeure, LIPN, Université Sorbonne
Paris Nord.
Examinatrice: Emmannuelle Encrenaz, Professeure, LIP6, Sorbonne
Université.
Directeur: Souheib Baarir, Enseignant-Chercheur, LRE, EPITA.
Encadrant: Étienne Renault, SiPearl.
Résumé :
Les systèmes informatiques sont devenus omniprésents dans notre vie
quotidienne. Garantir la fiabilité
et la robustesse de ces systèmes est une nécessité absolue. La
Vérification de Modèles (Model Checking)
est l'une des approches dédiées à cette fin. Son objectif est de prouver
l'absence de défaillances ou
d'identifier d'éventuelles erreurs.
Le model checking se décline en plusieurs techniques. Parmi celles-ci,
on trouve la Vérification de
Modèles Bornée (Bounded Model Checking - BMC), une technique qui repose
sur la satisfiabilité
booléenne (SAT). L'idée centrale derrière le BMC est de vérifier qu'un
modèle, limité à des exécutions
bornées par un entier k, satisfait sa spécification, définie comme un
ensemble d'expressions logiques
temporelles. Dans cette approche, les comportements du système sont
exprimés sous forme de problèmes SAT.
Contrairement à d'autres méthodes de vérification formelle, le BMC basé
sur SAT n'est généralement pas
sensible au problème de l'explosion de l'espace d'états, ce qui peut
poser problème lors de la conception
de systèmes impliquant des millions de variables et de contraintes.
Cependant, le compromis réside dans
la complexité temporelle, car les problèmes SAT sont connus pour être
NP-complets.
Au cours des dernières décennies, d'importantes avancées ont été
réalisées dans la résolution séquentielle
de problèmes SAT. Ces développements se sont principalement concentrés
sur l'utilisation d'informations
dynamiques, acquises lors du processus de résolution (par exemple,
l'apprentissage de clauses binaires) ou
d'informations statiques, extraites de la structure inhérente du
problème SAT (par exemple, la structure
en communauté). Toutefois, moins d'attention a été accordée aux
informations structurelles du problème
initial. Par exemple, lorsque qu'un problème BMC est réduit à une
formule booléenne, des données
cruciales sont perdues lors de la traduction. Comme le souligne cette
thèse, la réintégration de ces
informations perdues peut considérablement améliorer le processus de
résolution. Ce travail explore des
moyens d'améliorer la résolution de problèmes BMC basés sur SAT, tant
dans des contextes séquentiels que
parallèles, en exploitant et en valorisant les informations pertinentes
extraites des caractéristiques
inhérentes du problème. Cela peut impliquer l'amélioration
d'heuristiques génériques existantes ou la
décomposition efficace de la formule en partitions.
Cordialement,
Anissa Kheireddine
______________________
Annonce mailing list -- annonce(a)lrde.epita.fr
https://lists.lrde.epita.fr/postorius/lists/annonce.lrde.epita.fr//
______________________
Lrde mailing list -- lrde(a)lrde.epita.fr
https://lists.lrde.epita.fr/postorius/lists/lrde.lrde.epita.fr//
______________________
Current mailing list -- current(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/current.ml.lre.epita.fr//
______________________
Doctorants mailing list -- doctorants(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/doctorants.ml.lre.epita.fr//
______________________
Docs mailing list -- docs(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/docs.ml.lre.epita.fr//
______________________
Docs.toulouse mailing list -- docs.toulouse(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/docs.toulouse.ml.lre.epita.fr//
Bonjour tout le monde,
Dans le cadre des séminaires de l'équipe Sécurité /Systèmes, nous écouterons Yackolley Amoussou-Guenou, MCF à l'Université Paris-Panthéon-Assas et le centre de recherche CRED, jeudi 07/12/2023 à 10h30.
Yackolley Amoussou-Gueno nous parlera de ses travaux sur "Ethereum Proof-of-Stake under Scrutiny".
Résumé :
Ethereum has undergone a recent change called the Merge, which made Ethereum a Proof-of-Stake blockchain shifting closer to BFT consensus. Ethereum, which wished to keep the best of the two protocol designs (BFT and Nakomoto-style), now has a convoluted consensus protocol as its core. The result is a blockchain being possibly produced in a tree-like form while participants try to finalize blocks.
We categorize different attacks jeopardizing the liveness of the protocol. The Ethereum community has responded by creating patches against some of them. We discovered a new attack on the patched protocol.
To support our analysis, we propose a new high-level formalization of the properties of liveness and availability of the Ethereum blockchain, and we provide a pseudo-code. We believe this formalization to be helpful for other analyses as well. Our results yield that the Ethereum Proof-of-Stake has safety but only probabilistic liveness. The probability of the liveness is influenced by the parameter describing the time frame allowed for validators to change their mind about the current main chain. Joint work with Ulysse Pavloff and Sara Tucci-Piergiovanni (CEA-List, Université Paris-Saclay).
Bio :
Yackolley Amoussou-Guenou is associated professor (maître de conférences) in computer science at Université Paris-Panthéon-Assas, in the CRED research center. He was previously researcher at CEA-List, Université Paris-Saclay. He holds a PhD from Sorbonne Université and a M.Sc. from Université Paris Cité (ex- Paris-Diderot), both degrees in theoretical computer science.
He works on various aspects of distributed systems, and in particular on the blockchain technologies: the consensus protocols, the distribution of rewards, and the use of game theory to study the incentives. More generally, his research interests span from distributed systems to algorithmic game theory and their combination.
Cordialement,
Ghada Gharbi
________________________________________________________________________________
Réunion Microsoft Teams
Participez à partir de votre ordinateur, de votre application mobile ou de l’appareil de la salle
Cliquez ici pour rejoindre la réunion<https://teams.microsoft.com/l/meetup-join/19%3ameeting_ZGI5YzFhZGEtZDhiNi00…>
ID de la réunion : 355 366 181 466
Code secret : jSvE2T
Télécharger Teams<https://www.microsoft.com/en-us/microsoft-teams/download-app> | Rejoindre sur le web<https://www.microsoft.com/microsoft-teams/join-a-meeting>
Pour en savoir plus<https://aka.ms/JoinTeamsMeeting> | Options de réunion<https://teams.microsoft.com/meetingOptions/?organizerId=7c5194f6-08ca-45e8-…>
________________________________________________________________________________
______________________
Doctorants mailing list -- doctorants(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/doctorants.ml.lre.epita.fr//
______________________
Docs mailing list -- docs(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/docs.ml.lre.epita.fr//
______________________
Docs.toulouse mailing list -- docs.toulouse(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/docs.toulouse.ml.lre.epita.fr//
Bonjour tout le monde,
Dans le cadre des séminaires de l'équipe Sécurité /Systèmes, nous écouterons Yackolley Amoussou-Guenou, MCF à l'Université Paris-Panthéon-Assas et le centre de recherche CRED, jeudi 07/12/2023 à 10h30.
Yackolley Amoussou-Gueno nous parlera de ses travaux sur "Ethereum Proof-of-Stake under Scrutiny".
Résumé :
Ethereum has undergone a recent change called the Merge, which made Ethereum a Proof-of-Stake blockchain shifting closer to BFT consensus. Ethereum, which wished to keep the best of the two protocol designs (BFT and Nakomoto-style), now has a convoluted consensus protocol as its core. The result is a blockchain being possibly produced in a tree-like form while participants try to finalize blocks.
We categorize different attacks jeopardizing the liveness of the protocol. The Ethereum community has responded by creating patches against some of them. We discovered a new attack on the patched protocol.
To support our analysis, we propose a new high-level formalization of the properties of liveness and availability of the Ethereum blockchain, and we provide a pseudo-code. We believe this formalization to be helpful for other analyses as well. Our results yield that the Ethereum Proof-of-Stake has safety but only probabilistic liveness. The probability of the liveness is influenced by the parameter describing the time frame allowed for validators to change their mind about the current main chain. Joint work with Ulysse Pavloff and Sara Tucci-Piergiovanni (CEA-List, Université Paris-Saclay).
Bio :
Yackolley Amoussou-Guenou is associated professor (maître de conférences) in computer science at Université Paris-Panthéon-Assas, in the CRED research center. He was previously researcher at CEA-List, Université Paris-Saclay. He holds a PhD from Sorbonne Université and a M.Sc. from Université Paris Cité (ex- Paris-Diderot), both degrees in theoretical computer science.
He works on various aspects of distributed systems, and in particular on the blockchain technologies: the consensus protocols, the distribution of rewards, and the use of game theory to study the incentives. More generally, his research interests span from distributed systems to algorithmic game theory and their combination.
Cordialement,
Ghada Gharbi
________________________________________________________________________________
Réunion Microsoft Teams
Participez à partir de votre ordinateur, de votre application mobile ou de l’appareil de la salle
Cliquez ici pour rejoindre la réunion
ID de la réunion : 355 366 181 466
Code secret : jSvE2T
Télécharger Teams | Rejoindre sur le web
Pour en savoir plus | Options de réunion
________________________________________________________________________________
[cid:206faf58-e98c-4f57-afb4-99312c055790]<https://www.epita.fr/>
Ghada GHARBI
Enseignante - Chercheure
EPITA Toulouse
[cid:a1051f2e-87b2-4245-b32f-77bd4c872fd3]<https://www.facebook.com/epita/> [cid:51a3bc82-95ba-42e6-a531-a2aae2e65f85] <https://www.instagram.com/epita.national/> [cid:8dfe7ccb-c5af-41ec-9fa3-74e425bab26a] <https://www.linkedin.com/school/epita-ecole-ingenieurs-informatique> [cid:bee4ed5b-f540-4b37-9019-6661a176d062] <https://twitter.com/epita> [cid:76b31b86-fe95-4eb9-82fc-4b8e32c213f2] <https://www.epita.fr/> [cid:b28098f7-14b4-4078-8606-ef5ac44088c8] <https://www.youtube.com/channel/UC33NtVL7bStj4FmWeIstKqg>
______________________
Doctorants mailing list -- doctorants(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/doctorants.ml.lre.epita.fr//
______________________
Docs mailing list -- docs(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/docs.ml.lre.epita.fr//
______________________
Docs.toulouse mailing list -- docs.toulouse(a)ml.lre.epita.fr
https://lists.lrde.epita.fr/postorius/lists/docs.toulouse.ml.lre.epita.fr//