Talks
Qbricks, a core development framework for certified quantum programming
Due to the nature of quantum computation, we believe that, in this field, formal verification is meant to play a role similar to that of test development in classical computing. In this talk we present Qbricks, a core programming language for entirely verifiable quantum computing, embedded into Why3. Qbricks both provides programming functions such as in other programming languages and formal analysis means enabling to specify and verify the written programs. We believe this two layers approach is necessary for widespread verified programming methodology. We present our implementation of both the matrix and the path-sum semantics for quantum processes and the first fully verified equivalence proof between those. In addition, we implemented various further semantics artifacts for quantum circuits semantics. Thanks to Qbricks, we present a verified implementation of the phase estimation algorithm. This is, as far as we know, the first scale-invariant proof of a non-trivial quantum routine.
27/02/2020, Séminaire 68NQRT INRIA/IRISA, Rennes
30/01/2020, séminaire d'Informatique Théorique Université de Rouen
01/12/2019, séminaire Gallium, Inria, Paris
28/11/2019, Journées du groupe de travail Informatique Quantique, FEMTO, Besançon
26/11/2019, Réunion d'avancement, ANR project SoftQPro, Atos Bull, les Clayes sous Bois
16/10/2019, séminaire LSL, CEA/LIST, Palaiseau
04/10/2019, séminaire VALS, LRI, Gif sur Yvette
Knowledge about the context and knowledge about the past, in a strategic context
In this talk, we investigate the question of mutual moves observations between agents, in a strategic context. This question is closely linked to the observance of the past for agents: an agent 'a' (partially) observes another agent's ('b') moves in a semantic game if at each time of the game she knows (something about) the strategy played by 'b' so far. Therefore, we introduce PKSL, a strategy logic with knowledge framework and backward looking time operators. We illustrate the characterization of moves observations in this setting. PKSL also provides synctactical characterizations of memory and consciousness about the flow of time for agents. These properties classically refer to meta-logical options, encoded in the definitions for the semantics of languages. We raise questions concerning the convergence between such treatment of these properties and their partial synctactical characterization in PKSL, as open directions.(slides)
23/02/2017, workshop FMAI 2017, Naples
16/02/2017, séminaire 68NQRT, INRIA/IRISA, RENNES
Using dynamic modeling and model-checking for the analysis of IMA architectures interconnected with TTEnetworks: a NuSMV based solution
This talk presents the works achieved during a postdoctoral internship at Ecole Polytechnique de Montréal, under the supervision of prof. John Mullins. It was supported by the CRIAQ-NSERC RDC Project VerITTAS (Verification and Integration of multi-critical Time Triggered Avionics Systems) (AVIO613). This project aims at applying Model Driven Architectures to build Time Triggered Architectures (TTA), defining models and automatic techniques for developing and integrating TTA based mixed criticality avionic systems, and experimenting integrated modular avionics (IMA) systems using TTA based data communication networks. In these works, we consider as inputs the schedulings given for IMA architectures and time-triggered frames in TT-Ethernet networks, we provide a dynamic modeling for the resulting system based on discrete time, and a formalization for the behavior of this system. This enables:
to simulate and analyze the behavior of the systems characterized by these schedulings,
to generalize the computation means for the exact worst case transmission delay of rate constrained frames in the network to any system, whatever the topology of the network,
to check temporal specifications for a system
to compute the worst-case delay for the executions of complexe functionality chains, involving both computations in IMA components and transmissions through the network.
16/12/2016, réunion d'avancement, projet VeriTTas (Avio 613)
A Formal Treatment of Agents, Goals and Operations using Alternating-Time Temporal Logic
The aim of this talk is to present a formal framework for actor- and goal-oriented requirements engineering modelling. To do so, we define Khi, a core modelling language, as well as its semantics in terms of a strategy logic we call SLsc. Actors, concrete active entities, are defined by their capabilities. They also pursue behavioural goals that are realised by operations. Then a relation of assignment, between (coalitions of) actors and roles (sets of operation specifications) is defined. We highlight the importance of this relation by exhibiting three "assignment problems" and we define criteria for their correctness. They are modalities about the effective ability of (coalitions of) actors to play their assigned roles. The assignment problems reduce to the satisfaction of Slsc formulas in a structure derived from the capabilities of actors. Thanks to the properties of SLsc, we end up with a decidable procedure for the assignment problems. We illustrate our approach using a toy example featuring a satellite-based Earth observation mission.(Slides)
16/05/2011, séminaire DTIM, Toulouse
19/12/1012, workshop MFDL, Paris
Vers une sémantique des jeux pour un langage d’ingénierie des exigences par buts et agents
Cet exposé propose des structures d’interprétation pour le langage KHI, un langage de modélisation pour l’ingénierie des exigences, qui formalise notamment les notions d’agents, de buts et d’opérations. Deux notions d’agents s’y confrontent : les acteurs, qui sont les agents présents et décrits par leurs capacités d’action sur le système, et les rôles, qui décrivent le comportement attendu des agents pour la réalisation des buts. Les rôles sont ensuite assignés à des acteurs ou des coalitions d’acteurs. La capacité effective des coalitions à jouer les rôles qui leur sont assignés fournit donc un critère de correction du modèle, on appelle le problème relatif problème de l’assignation. KHI a une sémantique formelle dans un fragment de la logique temporelle multiagents ATL*, nommé ATLKHI . Nous décrivons les modèles sémantiques qui permettent d’interpréter ATLKHI et de réduire le problème de l’assignation à un problème de model-checking.(Slides)
05/04/2012, journées FAC, Toulouse
23/01/2012, séminaire DTIM, Toulouse
11/06/2012, séminaire LACL , Créteil
Updatable Strategy Logic
This presentation is about temporal multi-agent logics. Several of these formalisms have been already presented (ATL-ATL*, ATLsc, SL). They enable to express the capacities of agents in a system to ensure the satisfaction of temporal properties. Particularly, SL and ATLsc enable several agents to interact in a context mixing the different strategies they play in a semantical game. We generalize this possibility by proposing a new formalism, Updating Strategy Logic (USL). In USL, an agent can also refine its own strategy. The gain in expressive power rises the notion of ``sustainable capacities'' for agents. USL is built from SL. It mainly brings to SL the two following modifications: semantically, the successor of a given state is not uniquely determined by the data of one choice from each agent. Syntactically, we introduce in the language an operator, called an ``unbinder'', which explicitely deletes the binding of a strategy to an agent. We show that USL is strictly more expressive than SL. We also give the results of model-checking for USL and its memoryless version. They are the same as those of formalisms with implicit unbinders, such as SL and ATLsc.(Slides)
09/05/2017, workshop CELLO, Nancy
17/04/2014, journées FAC, Toulouse
20/06/2013, séminaire Inria, Rennes
20/06/2013, séminaire LSV , Cachan
08/01/2013, séminaire IRIT, Toulouse
Formal modelling of requirements and temporal multi-agent logics
See phD defense
27/11/2014, BRICS seminary, Aarlborg