Lien iCal public : https://calendar.google.com/calendar/ical/proval%40lri.fr/public/basic.ics
Seminars
Formal Verification of BDI Agents
Speaker: Jim Woodcock, University of York (Emeritus)
Tuesday 2025-02-11 14:00, Room to be announced
Abstract:
In this talk, we unveil a powerful formal modelling framework for the Belief-Desire-Intention (BDI) agent paradigm, combining the strengths of Isabelle/HOL and Z-Machines. The BDI architecture is a cornerstone for designing intelligent agents who think, plan, and act by maintaining beliefs about their world, pursuing ambitious goals (desires), and executing intentions to turn those goals into reality.
Our approach introduces a general-purpose formal model of BDI systems, meticulously crafted using Z-Machines. This framework captures the full spectrum of agent behaviour, from beliefs and actions to rules, plans, pattern matching, and rule applications. But we don't stop at modelling: through the precision of Hoare Logic and the expressive power of Isabelle/Z-Machines, we enable formal verification of an agent's behaviour, ensuring its decisions are not just intelligent but provably correct.
What makes this exciting? By blending automated reasoning with compositional verification techniques, our framework can uncover hidden bugs, verify critical invariants, and establish high-level system properties. To bring this to life, we present a case study featuring a nuclear inspector robot: an intelligent agent with a high-stakes mission. Our method verifies its behaviour and identifies subtle flaws, hinting at the value of formal verification in real-world applications.
This work pushes the boundaries of agent-based systems, demonstrating how rigorous formal methods can unlock trust and reliability in intelligent agents. It's not just about smarter agents; it's about agents you can trust when it matters most.
This is joint work with Thomas Wright (Aarhus), Louise Dennis (Manchester), and Simon Foster (York).
Agenda
Séminaires antérieurs
Formal Methods for Modern Payment Protocols
Speaker: David Basin, Prof. Dr . David Basin, Chair of the Computer Security Group, ETH Zürich
Tuesday 8th April 2025, 14:00, Room to be announced
Abstract: EMV is the international protocol standard for smartcard payments and is used in billions of payment cards worldwide. Despite the standard’s advertised security, various issues have been previously uncovered, deriving from logical flaws that are hard to spot in EMV’s complex specification, running over 2,000 pages.
We have formalized various models of EMV in Tamarin, a symbolic model checker that we developed for cryptographic protocols. Tamarin was extremely effective in finding critical flaws, both known and new. For example, we discovered multiple ways that an attacker can use a victim's EMV card (e.g., Mastercard or Visa Card) for high-valued purchases without the victim's supposedly required PIN. Said more simply, the PIN on your EMV card is useless! We report on this, as well as followup work with an EMV consortium member on verifying the latest, improved version of the protocol, the EMV Kernel C-8. Overall our work provides evidence that security protocol model checkers like Tamarin have an essential role to play in developing critical, real-world cryptographic protocols, and that they are up to this challenge.
Formalised meta-theory for a certified type-theoretic kernel
Speaker: Meven LENNON-BERTRAND, University of Cambridge,mgapb2@cam.ac.uk
Tuesday 2024-12-17 14:00, Room to be announced
Abstract:
Proof assistant kernels are a natural target for program certification: they are critical, yet small and well-specified. Still, despite the maturity of type theory and software verification, we are yet to see a certified Agda, Coq or Lean. In my talk, I will give an overview of the landscape around this grand goal, more particularly of the interaction between certification and meta-theory, and present two complementary formalisation projects in that direction.
The core difficulty is that kernels rely on complex invariants, which in turn rest on significant properties of the type system. In essence, we cannot certify a kernel without first formalising the meta-theory of its type system. Historically, emphasis has been put on the *normalisation* property. I will explain why, in my view, other properties are more important, in particular the one called *injectivity of type constructors*.
Strict Categories with Families
Speaker: Loic Pujet, University of Stockholm, loic@pujet.fr
Tuesday 26 Nov 2024, 14:00, Room 1Z56
Abstract:
Categories with families (CwF) are perhaps the most widely used notion of models for dependent types. They can be described by an algebraic signature with dependent sorts for contexts, substitutions, types and terms, as well as a plethora of constants and equations. Unfortunately, this mix of dependent sorts and equations is particularly prone to transport hell, and in practice it is nearly impossible to prove non-trivial results using CwFs in a proof assistant.
In this talk, I will present a method based on Pédrot's "prefascist sets" to strictify (nearly) all the equations of a CwF, so that they hold by definition. I will then discuss applications of this method to formal proofs of canonicity and normalisation.
This is joint work with Ambrus Kaposi.
Lindenmayer graph languages, first-order theories and expanders
Speaker: Teodor Knapik, Université de la Nouvelle-Calédonie, Nouméa
Tuesday 14 May 2024, 14:00, Room 1Z56
Abstract: Imagined by Kolmogorov in the middle of past century, expanders form remarkable graph families with applications in areas as diverse as robust communication networks and probabilistically checkable proofs, to name just two. Since the proof of the existence of expanders, it took several years to come up with an explicit algebraic construction [Margulis 1973] of some expander families. Their first elementary (combinatorial) construction has been published in 2002 and awarded Gödel Prize in 2009.
In this talk, we introduce a framework that captures most of the known combinatorial constructions of expanders. It is based on a generalisation of Lindenmayer systems to the domain of graphs. We call this formalism Lindenmayer graph grammars. We identify a few essential properties which make decidable the language checking problem with respect to first-order sentences. This result is obtained by encompassing a graph language into an automatic structure. By language checking in this specific context, we mean the following problem.
Instance: a Lindenmayer graph grammar and a first-order sentence. Question: Does there exist a graph in the language for which the sentence holds?
Keynote: Challenges and triumphs of verification in the CSP style
Speaker: Bill Roscoe Emeritus professor, University of Oxford, GB
Thursday (!) May 23 2024, 14:00, Room 1Z56
Abstract: I have been doing practical verification in CSP, its tools and models for 40 years. The main challenge has been packaging this for the industrial engineer. I will discuss how this has been solved in the Coco System www.cocotec.io, which is used for object based development of massive systems in industry. Separately I will show how I have used it to underpin a highly innovative blockchain consensus protocol by using it to model decentralised, partly malevolent systems.
Static analysis and model reduction for a site-graph rewriting language
Speaker: Jérôme Feret ENS Ulm, jerome.feret@ens.psl.eu
Tuesday Mar 26 2024, 14:00, Room 1Z56
Abstract: Software sciences have a role to play in the description, the organization, the execution, and the analysis of the molecular interaction systems such as biological signaling pathways. These systems involve a huge diversity of bio-molecular entities whereas their dynamics may be driven by races for shared resources, interactions at different time- and concentration-scales, and non-linear feedback loops. Understanding how the behavior of the populations of proteins orchestrates itself from their individual interactions, which is the holy grail on systems biology, requires dedicated languages offering adapted levels of abstraction and efficient analysis tools.
In this talk we describe the design of formal tools for Kappa, a site-graph rewriting language inspired by bio-chemistry. In particular, we introduce a static analysis to compute some properties on the biological entities that may arise in models, so as to increase our confidence in them. We also present a model reduction approach based on a study of the flow of information between the different regions of the biological entities and the potential symmetries. This approach is applied both in the differential and in the stochastic semantics.
Atomic congestion games with non-separable costs: an application to smart charging
Speaker: Yezekaël Hayel, Université d'Avignon
Tuesday March 12 2024, 14:00, Room 1Z56
Abstract: Atomic congestion games with separable costs are a specific type of non-cooperative games with a finite number of players where the cost of a commodity depends on the number of players choosing it. But in many applications, resources may be correlated in the sense that the resource cost may depend on the usage of other resources, and thus cost function is non-separable. This is the case for traffic models with opposite directions dependencies, resource graph games, and smart charging games to cite a few examples. In this talk, after introducing the concepts of atomic congestion games with non-separable costs, a specific smart charging game will illustrate such game theoretical framework. In this particular setting, we prove the existence of pure Nash Equilibrium by showing ordinal potential function existence. We also demonstrate the convergence of a simple Reinforcement Learning algorithm to the pure NE for both synchronous and asynchronous versions. Finally, the recent framework of Resource Graph Games will be presented. In this setting, dependencies between resources are modeled as an oriented graph. This new framework generalizes atomic congestion games with non-separable costs and opens new questions about the existence and uniqueness of pure NE in this general setup.
Solving Quantified Boolean Formulas and its Applications
Speaker: Martina Seidel, Johannes Kepler University, Linz, Austria
Tuesday Feb 20 2024, 14:00, Room 1Z53
Abstract: Quantified Boolean Formulas (QBFs) extend propositional logic by quantifiers over the Boolean variables. Despite the PSPACE hardness of their decision problem, much progress has been made in practical solving, making QBFs an attractive framework for encoding various problems from artificial intelligence and formal verification.
In this talk, we will give an overview on recent trends and developments in QBF solving and we will discuss promising applications of QBFs.
Modèles de Langage
Speaker: Gustave Cortal, LMF
Tuesday Feb 06 2024, 14:00, 1Z71
Abstract: Je propose d'introduire certains concepts clés du traitement automatique des langues. Le cours se concentre sur les modèles de langage, qui sont des modèles prédictifs calculant la probabilité d’une séquence de mots, et trouvant des applications en traduction, résumé de texte, agent conversationnel, etc.
Je parlerai de différentes architectures utilisées dans l’histoire pour la modélisation statistique du langage, comme les n-grammes, les réseaux de neurones feed-forward, les réseaux de neurones récurrents et les transformers. Les avantages et les inconvénients de chaque architecture seront exposés. À la fin, il sera possible de comprendre conceptuellement comment un modèle comme ChatGPT fonctionne.
Logics for Strategic Reasoning: Recent Developments and Application to Mechanism Design
Speaker: Munyque Mittelmann, University of Naples
Tuesday, 12 December 2023, 14:00, Room 1Z71
Abstract: In recent years a wealth of logic-based languages have been introduced to reason about the strategic abilities of autonomous agents in multi-agent systems. This talk presents some of these important logical formalisms, namely, the Alternating-time Temporal Logic and Strategy Logic. We discuss recent extensions of those formalisms to capture different degrees of satisfaction, as well as to handle uncertainty caused by the partial observability of agents and the intrinsic randomness of MAS. Finally, we describe the recent application of those formalisms for Mechanism Design and explain how they can be used either to automatically check that a given mechanism satisfies some desirable property, or to produce a mechanism that does it.