TBA

TBA

TBA

TBA

For the analysis of concurrent programs, higher-dimensional automata (HDA) are models that help to limit the combinatorial explosion that can be observed with interleaving models. Such an automaton has a fundamentally geometric interpretation: it can be seen as a construction plan indicating how to glue together elementary topological spaces such as segments, squares, cubes, etc. In order to retrieve the semantics of the program in the topological space previously constructed, the latter must have a notion of local direction. To axiomatize this idea of local direction, several non-equivalent approaches have been proposed in the literature, such as d-spaces, streams, locally ordered spaces and so on.

In this talk, we present a unified framework, inspired by topological spaces, which can contain and compare these different approaches, and, more generally, in which it is possible to define all kinds of locally structured spaces. We show that many topological notions generalize to this framework, and that streams have a natural place in it.

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.