Lien iCal public : https://calendar.google.com/calendar/ical/proval%40lri.fr/public/basic.ics
Seminars
Agenda
Séminaires antérieurs
Towards Security-Oriented Program analysis
Speaker: Sébatien Bardin, CEA, Paris-Saclay
Tuesday 7 September 2021, 11:00, (amphi 1Z53, ENS Paris-Saclay)
Abstract: While digital security concerns increase, we face both a urging demand for more and more code-level security analysis and a shortage of security experts. Hence the need for techniques and tools able to automate part of these code-level security analyses. As source-level program analysis and formal methods for safety-critical applications have made tremendous progress in the past decades, it is extremely tempting to adapt them from safety to security. Yet, security is not safety and, while still useful, a direct adaptation of safety-oriented program analysis to security scenarios remains limited in its scope. In this talk, we will argue for the need of security-oriented program analysis. We will first present some of the new challenges faced by formal methods and program analysis in the context of code-level security scenarios. For example, security-oriented code analysis is better performed at the binary level, the attacker must be taken into account and practical security properties deviate from standard reachability / invariance properties. Second, we will discuss some early results and achievements carried out within the BINSEC group at CEA LIST. Especially, we will show how techniques such as symbolic execution and SMT constraint solving can be tailored to a number of practical code-level security scenarios.
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
Speaker: Léon Gondelman, Aarhus University, DK
Tuesday 15.6.2021, 11:00, online
Abstract: In this presentation we are going to talk about modular specification and verification of causally-consistent distributed database, a data structure that guarantees causal consistency among replicas of the database.
With causal consistency, different replicas can observe different data on the same key, yet it is guaranteed that all data are observed in a causally related order: if a node {$N$} observes an update {$X$} originating at node {$M$}, then node {$N$} must have also observed the effects of any other update {$Y$} that took place on node {$M$} before {$X$}. Causal consistency can, for instance, be used to ensure in a distributed messaging application that a reply to a message is never seen before the message itself.Read more...
Controlling a random population
Speaker: Pierre Ohlmann, IRIF
Tuesday 6.4.2021, 11:00, online
Abstract: Bertrand et al. introduced a model of parameterised systems, where each agent is represented by a finite state system, and studied the following control problem: for any number of agents, does there exist a controller able to bring all agents to a target state? They showed that the problem is decidable and EXPTIME-complete in the adversarial setting, and posed as an open problem the stochastic setting, where the agent is represented by a Markov decision process. In this paper, we show that the stochastic control problem is decidable. Our solution makes significant uses of well quasi orders, of the max-flow min-cut theorem, and of the theory of regular cost functions. We introduce an intermediate problem of independent interest called the sequential flow problem, and study the complexity of solving it.
Towards synthetic psychology: from phenomenology to cybernetics
Speaker: David Rudrauf
Tuesday 9.3.2021, 11:00, online
Abstract: The role of consciousness in biological cybernetics remains an essential yet open question for science. We introduce the Projective Consciousness Model (PCM) and show how its principles yield a unified model of appraisal and social-affective perspective taking and a method for active inference. We show how the PCM can account for known relationships between appraisal and distance as an inverse distance law, and how it can be generalised to implement Theory of Mind for strategic action planning. We use simulations of artificial agents applied to toy robots to demonstrate how different model parameters can generate a variety of emergent adaptive and maladaptive behaviours: from the ability to be resilient in the face of obstacles through imaginary projections, to the emergence of social approach and joint attention behaviours, and the ability to take advantage of false beliefs attributed to others. The approach opens new paths towards a science of consciousness, and applications, from clinical assessment to the design of artificial (virtual and robotic) agents. We discuss the interest and variety of computational challenges entailed by the approach. Read more...
Semantics for Variational Quantum Programming
Speaker: Vladimir Zamdzhiev, Inria/LORIA.
Tuesday March 15th 2022, 11:00, (online)
Abstract: In this talk, I will first introduce myself by briefly summarising my main research activities: (1) formal methods for diagrammatic reasoning about quantum information processing (e.g. higher-order rewriting of ZX-calculus diagrams); and (2) design and analysis of quantum programming languages. I will also explain how this fits perfectly within the research activities of the QuaCS team.
After that I will talk about some recent work on variational quantum programming that will appear in POPL 2022. The technical summary of this talk is below.
We consider a programming language that can manipulate both classical and quantum information. Our language is type-safe and designed for variational quantum programming, which is a hybrid classical-quantum computational paradigm. The classical subsystem of the language is the Probabilistic FixPoint Calculus (PFPC), which is a lambda calculus with mixed-variance recursive types, term recursion and probabilistic choice. The quantum subsystem is a first-order linear type system that can manipulate quantum information. The two subsystems are related by mixed classical/quantum terms that specify how classical probabilistic effects are induced by quantum measurements, and conversely, how classical (probabilistic) programs can influence the quantum dynamics. We also describe a sound and computationally adequate denotational semantics for the language. Classical probabilistic effects are interpreted using a recently-described commutative probabilistic monad on DCPO. Quantum effects and resources are interpreted in a category of von Neumann algebras that we show is enriched over (continuous) domains. This strong sense of enrichment allows us to develop novel semantic methods that we use to interpret the relationship between the quantum and classical probabilistic effects. By doing so we provide a very detailed denotational analysis that relates domain-theoretic models of classical probabilistic programming to models of quantum programming.