[[index|{{ scalplogo.png?400}}]]
===== Journées 2024 du GT Scalp =====
==== Du 18 au 20 novembre 2024 à Lille ====
* [[gt-scalp:journees-2024#introduction|Introduction]]
* [[gt-scalp:journees-2024#orateurs_invites|Oratrices et orateurs invités]]
* [[gt-scalp:journees-2024#inscriptions_et_propositions_d_expose|Inscriptions et propositions d'exposé]]
* [[gt-scalp:journees-2024#informations_pratiques|Informations pratiques]]
* [[gt-scalp:journees-2024#programme_preliminaire|Programme]]
* [[gt-scalp:journees-2024#liste_des_exposes_contribues|Liste des exposés contribués]]
* [[gt-scalp:journees-2024#participants|Participants]]
* [[gt-scalp:journees-2024#comite_d_organisation|Comité d'organisation]]
==== Introduction ====
Les rencontres 2024 du [[http://www.irif.fr/gt-scalp/|GT Scalp]] se tiendront à Lille du 18 au 20 novembre.
Cette année, nos rencontres annuelles sont organisées conjointement avec le GT Verif du GDR-IFM qui suivront immédiatement, deux demi-journées étant organisées en commun aux deux GT, les mardi après-midi et mercredi matin: l'événement global Scalp-Verif s'étendra donc du 18 novembre au 21 novembre.
Les journées SCALP débuteront lundi en milieu de journée et s'achèveront mercredi en début d'après-midi:
* Lundi après-midi et mardi matin seront consacrées à des journées spécifiquement SCALP;
* Mardi après-midi et mercredi matin seront consacrées à des journées conjointes SCALP-Vérif;
* Mercredi après-midi et jeudi matin seront consacrées à des journées spécifiquement Vérif.
/*
^ ^ Lundi ^ Mardi ^ Mercredi ^ Jeudi ^
| Matin | | Scalp | Scalp-Verif | Verif |
| Après-midi | Scalp | Scalp-Verif | Verif | |
*/
/*
[[https://framaforms.org/journees-scalp-2023-1694759470 |Les inscriptions sont ouvertes]], les informations sur les exposés invités et contribués, ainsi que l'organisation pratique des journées se trouvent ci-dessous.
*/
Les informations sur les exposés invités et contribués, l'inscription ainsi que l'organisation pratique des journées seront rogressivement complétées ci-dessous.
==== Exposés invités ====
* [[https://people.irisa.fr/David.Baelde/|David Baelde]], IRISA, Ens Rennes, **//Proof-theoretical investigations into Squirrel & CCSA logics
//** [[https://www.irif.fr/_media/gt-scalp/journees-2024/scalp24_baelde.pdf|(slides)]]
In this talk, I will give an overview of a particular logic-based methodology for proving security protocols, based on so-called CCSA logics and implemented in the Squirrel proof assistant, and I will more specifically present recent proof-theoretical results about a modal fragment of that logic.
CCSA logics have been proposed by Bana and Comon in 2012 as a logic-based approach to reason about cryptographic protocols. Initially based in first-order logic and aimed for full automation, the core ideas of CCSA logics have been adapted to richer logical settings in a recent line of work. As a result, mechanized proofs of several protocols have been developed using the Squirrel proof assistant, which implements a rich, higher-order CCSA logic.
One of the key ingredients in Squirrel's logic is the notion of "overwhelming truth". Cryptographers consider that asymptotic security holds when, for any possible attacker running in polynomial time, the probability that the attack succeeds is negligible, i.e. that it tends fast enough to zero with the size of secrets. In order to reason formally about cryptographic truth, one may thus consider logics where a formula is satisfied when it is true with overwhelming probability, i.e. a probability that tends fast enough to one with the size of secrets. Squirrel implements one such logic, but it relies on an ad-hoc proof system for overwhelming truth. To improve this situation, we have recently studied a propositional fragment of Squirrel's logic under the lens of modal logic. We first consider a modal logic of overwhelming truth, and show that it coincides with S5. In addition to providing an axiomatization, this brings a well-behaved proof system for our logic in
the form of Poggiolesi’s hypersequent calculus. We then consider a logic that is closer to Squirrel’s language, where the overwhelming truth modality cannot be nested. In that case, we show that a simple proof system, based on regular sequents, is sound and complete. This result justifies the core of Squirrel’s proof system.
SC-TPTP est une extension du format TPTP (Thousands of Problems for Theorem Provers) conçue pour intégrer les preuves basées sur les séquents dans un cadre standardisé. En effet, ben qu'étant un standard dans la communauté de preuve automatique, le format SC-TPTP ne permet pas la représentation de preuves basées sur les séquents. Ces preuves sont pourtant très intéressantes, car elles se traduisent naturellement vers des assistants de preuve, permettant ainsi la génération de certificats de preuves. SC-TPTP remédie à cette limitation en ajoutant une expressivité supplémentaire au format, permettant de formaliser ces preuves tout en restant compatible avec les outils et formats existants. Le format est également conçu comme un format d’échange entre les prouveurs automatiques et interactifs. L’un des objectifs clés de SC-TPTP est de répondre à un besoin fondamental : éviter la prolifération des formats et des standards dans la communauté. En unifiant les représentations de preuves, SC-TPTP simplifie le développement d'outils de preuve, réduit la complexité des conversions entre formats et permet une adoption plus large de diverses approches de preuves. En parallèle, SC-TPTP s’accompagne d'une bibliothèque d'outils, SC-TPTP Utilities, incluant des prouveurs/assistants de preuve capables de générer/importer et valider des preuves au format SC-TPTP, ainsi que des outils de traduction permettant l’export vers d’autres systèmes de preuves interactifs comme Coq, facilitant ainsi encore plus l'interopérabilité.
The approach of verifying programs by means of an embedding Separation Logic in an interactive theorem prover has been developed over the past two decades. It has proved to be the tool of choice for the verification of data structures and algorithms with complex invariants. Moreover, work from last decade has shown how to generalize the approach for reasoning about concurrent programs, as well as for establishing time and space bounds. In this talk, I will give an overview of this state-of-the-art technology, focusing on sequential programs, and I present a demo of the CFML tool.
In short, no.
The origin of the trouble seems to be the title of a
1998 paper by A. Jung and R. Tix entitled "the troublesome
probabilistic powerdomain". It seems that this has now
come to be interpreted as justifying that one has to look
beyond domain theory and dcpos to give semantics to
higher-order probabilistic languages - and this interpretation
is bogus.
There is simply no problem giving semantics to such
languages in terms of plain old dcpo semantics. Even
classical theorems such as soundness and adequacy
hold, a topic that I will touch only briefly.
One issue, though, is that the classical probabilistic
powerdomain monad is not known to be commutative.
This is easily solved by replacing it by a variant.
The simplest one is the monad of minimal valuations, but
there are other choices, too.
Although not all continuous valuations are minimal,
enough of them are. This allows us to give semantics to a
statistical programming language, with not just
higher-order and probabilistic features, but also
continuous distributions on exact real numbers (and
soft conditioning: Lebesgue measure, and in fact any
measure on the real numbers, induces a continuous valuation on the
domain of exact reals that is in fact a minimal valuation.
I will finish the presentation by giving a proof
that there are dcpos on which not all continuous
valuations are minimal; but this is hard to find,
and not that simple to prove.
In the game-theoretic approach toward controller synthesis, we model the interaction between a system to control and its environment as (some variation of) game between these entities, and we are looking for an appropriate (e.g., winning or optimal) strategy of the system. This strategy then constitutes a formal blueprint for a real-world controller for the system. The general consensus is that simple (e.g., using limited memory) strategies are better: corresponding controllers will be easier to conceive and understand, and cheaper to produce and maintain. This talk focuses on the complexity of strategies in a variety of synthesis contexts. We will discuss recent results regarding memory and randomness, and take a quick glance at what lies beyond our traditional ways of understanding the notion of complexity for strategies.
We present an conservative extension of the notion of
recognizability to simply typed lambda-calculus. This notion allows to
solve syntactic problem in a general manner. We will present two
examples: parsing in a very general setting and higher-order
verification.
Decisiveness of infinite Markov chains with respect to some (finite or infinite) target set of states is a key property that allows to compute the reachability probability of this set up to an arbitrary precision. Most of the existing related works assume constant weights for defining the probability of a transition in the considered models. However numerous probabilistic modelings require (dynamic) weights that depend on both the current state and the transition. So we study and demonstrate that in the dynamic settings, the decisiveness is undecidable for both probabilistic one-counter machines and polynomial probabilistic Petri nets. Fortunately, we succeed to identify some interesting subclasses for which either the decisiveness is decidable in polynomial time or the models themselves are decisive with respect to a finite set.