TBA

TBA

TBA

TBA

CrewAI is a framework for orchestrating role-playing AI agents, collaborating to solve complex tasks. Here we introduce an innovative approach to formal verification that addresses the state explosion problem through a multi-agent AI framework, currently in early development stages. Our system deploys four specialized agents (State Representation Specialist, Abstraction Engineer, UPPAAL Interface Specialist, and Evaluation Specialist) that collaborate to analyze, optimize, and verify state spaces in formal models. This work represents a first step toward making formal verification more practical for complex systems through AI-assisted state space optimization.

Kleene Algebra with Tests (KAT) provides a framework for algebraic equational reasoning about imperative programs. The recent variant Guarded KAT (GKAT) allows to reason on non-probabilistic properties of probabilistic programs. Here we introduce an extension of this framework called approximate GKAT (aGKAT), which equips GKAT with a partially ordered monoid (real numbers) enabling to express satisfaction of (deterministic) properties except with a probability up to a certain bound. This allows to represent in equational reasoning ‘à la KAT’ proofs of probabilistic programs based on the union bound, a technique from basic probability theory. We show how a propositional variant of approximate Hoare Logic (aHL), a program logic for union bound, can be soundly encoded in our system aGKAT. We then illustrate the use of aGKAT with an example of accuracy analysis from the field of differential privacy.

For concurrent programs, Higher Dimensional Automata (HDA) are a very expressive model of non-interleaving concurrency. In this talk, I explain my recent works regarding these models and its timed version.

Temporal logics are a powerful tool to specify properties of computational systems.
HDA recognize languages of partially ordered multisets, or pomsets. Recent work has shown that Monadic Second Order (MSO) logic is as expressive as HDA for pomset languages.
In recent work, we investigate the class of pomset languages that are definable in First Order (FO) logic. In the case of words, Kamp’s theorem states that FO is as expressive as Linear Temporal Logic (LTL). Our aim is to prove a variant of Kamp’s theorem for pomset languages. Thus, we define a temporal logic called Sparse Pomset Temporal Logic (SPTL), and show that it is equivalent to FO, when there is no auto-concurrency.
In previous work, we worked on lifting decidability and undecidability results from Timed Automata to a timed version of HDA, Higher Dimensional Timed Automata.

Cette présentation résume mes travaux de thèse autour de TLA+ et de son système de preuves. TLA+ est un langage de spécification basé sur la théorie des ensembles non typée. Son prouveur, TLAPS, génère et encode des obligations de preuve pour différents solveurs externes. Je me suis intéressée à l’encodage SMT dans l’optique de le rendre plus sûr d’utilisation, car il est apparu que l’ancienne version contenait des bugs. Je commencerai par exposer les bases de TLA+, puis je décrirai les étapes essentielles de l’encodage. L’innovation principale de ces travaux est le recours aux « triggers » de SMT, qui ont permis d’optimiser l’instanciation au premier ordre et de rendre l’encodage efficace en pratique.

Timing leaks in timed automata (TA) can occur whenever an attacker is able to deduce a secret by observing some timed behavior. In execution-time opacity, the attacker aims at deducing whether a private location was visited, by observing only the execution time. It can be decided whether a TA is opaque in this setting. In the work presented in this talk, we tackle control, and show that we are able to decide whether a TA can be controlled at runtime to ensure opacity. Our method is constructive, in the sens that we can exhibit such a controller.

Les assistants de preuves basés sur les types dépendants sont parmis les outils offrant les garanties les plus fortes sur la sécurité d’un logiciel. Cependant, pour des projets pratiques et de grande envergure, ils induisent un effort de preuve conséquent limitant leur adoption. Une situation communément rencontrée est l’utilisation de types de données efficaces, mais qui se prêtent peu au raisonnement, rendant les preuves très techniques. Une solution potentielle pour gérer cette complexité repose sur le principe d’univalence, proposé par Voevodski, qui postule que la bonne notion d’égalité entre les types est celles d’isomorphismes. Ce principe permet de transporter les algorithmes et leur preuves portant sur un type de données se prêtant au raisonnement mais inefficace pour le calcul vers un type de données efficace pour le calcul, mais moins simple pour le raisonnement. Malheureusement, le principe d’univalence est incompatible avec celui d’unicité des preuves d’identités (UIP), un autre principe permettant souvent de simplifier les raisonnements. Cela signifie qu’en pratique, travailler avec le principe d’univalence nécessite de gérer les preuves d’identités finement, ce qui est complexe. Dans cet exposé, je vais présenter mes travaux et une direction de recherche pour simplifier cette tache. Cette direction s’appuye sur un outil que je développe appelé CaTT, permettant de décrire la structure algébrique des types d’identités. Je montrerais comment le travail dans cet outil peut être partiellement automatisé, et présenterai un plug-in de Coq permettant de générer des calculs sur les termes d’identités. Cela permet de réduire l’effort de preuve à fournir pour gérer les types d’identités.