The remarkable success stories of deep learning systems give the impression that large advanced neural networks are all we need, and they will eventually make all the symbolic techniques obsolete. This predicted death of symbolic techniques might or might not happen in the end. But I believe that at least in the…
Reinforcement learning (RL) presents a promising approach to solving highly non-linear control tasks that are often challenging for classical control methods. In this talk, we present a learner-verifier framework for solving control tasks in stochastic systems with formal guarantees on reachability, safety or reach-avoidance specifications. Given a specification and a…
The Bakery algorithm is a landmark algorithm for ensuring mutual exclusion among N processes that communicate via shared variables. Starting from existing TLA+ specifications, we use the recently developed IC3PO parameterized model checker to automatically compute inductive invariants for two versions of the algorithm. We compare the machine-generated invariants with…
Traditional separation logic-based shape analyses utilize inductive summarizing predicates so as to capture general properties of the layout of data-structures, to verify accurate manipulations of, e.g., various forms of lists or trees. However, they also usually abstract away contents properties, so that they may only verify memory safety and invariance…
We investigate the impact of potential symmetries in site-graph rewriting rules on the overall behavior of the system which are induced by these rules. For this purpose, we introduce a categorical framework in which rules are seen as pairs of embeddings, the application of a rule as a universal construction…
In this talk, I present several computability results in anonymous networks with broadcast communications. First, I recall the characterization, given by Hendrickx and Tsitsiklis, of the computable functions when agents have no information on their outgoing neighborhoods. Then I give the characterization of computable functions in networks with either (a)…
Proving that programs cannot crash is important, especially in embedded programs that are critical. The abstract interpretation framework gives tools to prove such properties at scale. Expressing complex properties on program states (the possible values of variables at given program points) can be very costly. This is why symbolic methods…
We present communication closed Distal protocol in two steps: 1) We introduce synchronization tags that capture the round numbers in synchronous protocols, 2) We show how to use this synchronization tag to reduce an asynchronous execution into a sequential one.
Much discussion exists about what is computation, but less about what is a computational problem. In the sequential setting, Turing’s definition of computational problem was based on functions. In a concurrent setting, various notions of distributed problems have been used, under different models of computation, ranging from models equivalent to…
In the last decades, logical or discrete models have emerged as a successful paradigm for capturing and predicting the behaviors of systems of molecular interactions. Intuitively, they consist in sampling the abundance of each kind of biochemical entity within finite sets of intervals and deriving transitions accordingly. On one hand,…
In recent years, the importance of data science applications to analyse phenomena in different areas of knowledge has increased, so it has become essential to verify the correctness of this type of programs. One of the ways in which a data science application can be verified is through the analysis…
Data science plays a crucial role in critical decision making in a variety of fields, including healthcare, finance, and avionics. Therefore, disastrous outcomes may result from programming errors in these safety-critical settings, especially when they do not result in software failures but instead produce a plausible yet erroneous outcome. Such…
Data dissemination is a fundamental task in distributed computing. This talk will explore broadcast problems in various innovative models where the communication network connecting n processes is dynamic (e.g., due to mobility or failures) and controlled by an adversary. In the main model, the processes transitively communicate their ids in…
The aim of this thesis is to explore and develop the application of abstract interpretation techniques to the context of machine learning. While big data and artificial intelligence have become widespread technologies, the lack of formal verification systems represents a serious limitation. Machine learning models can be very accurate but…
Imprecision is inherent in any decidable (sound) approximation of undecidable program properties. In abstract interpretation this corresponds to the release of false alarms, e.g., when it is used for program analysis and program verification. As all alarming systems, a program analysis tool is credible when few false alarms are reported.…
Formally describing the specification of a programming language is a challenging task. Specifications that use imperative features, such as state or exceptions, or that manipulate continuations are very difficult to describe in usual operational semantics, such as natural semantics or SOS.In addition, these descriptions are not objects that can be…
Symbolic execution is a program analysis technique commonly utilized to determine whether programs violate properties and, in case violations are found, to generate inputs that can trigger them. Used in the context of security properties such as noninterference, symbolic execution is precise when looking for counter-example pairs of traces when insecure information…
We propose a systematic approach to approximate the behavior of models of polymers synthesis/degradation, described in Kappa. Our abstraction consists in focusing on the behavior of all the patterns of size less than a given parameter. We infer symbolic equalities and inequalities which intentionally may be understood as algebraic constructions…
In this talk, we will discuss a symbolic representation for support vector machines (SVMs) by means of abstract interpretation. We leverage this abstraction in two ways: (1) to enhance the interpretability of SVMs by deriving a novel feature importance measure called abstract feature importance (AFI), that does not depend in any way on a given dataset of…
Separation logic-based shape analyses aim to infer properties of heap manipulating programs. These analyses abstract the heap using separation logic including inductive summarizing predicates. Whereas they have been successfully applied to prove properties of data structures layout, they usually abstract away some properties of the data structures contents. As a…
Probabilistic programming languages aim at designing and implementing algorithms that compute over probability distributions rather than states. They feature dedicated primitives for sampling and conditioning. Moreover, the evaluation of probabilistic programs relies on general purpose inference engines. In the last few years, several languages such as Pyro, Edward or Stan…
Asynchronous code is remarkably hard to get right, making it a common source of errors in TypeScript code. However, we would not be able to write TypeScript applications without it, because it enables long-running actions without freezing the current view. Developers usually rely on manual inspection to understand it, which is quite…
We consider networked systems in which each agent holds a certain variable, called clock, and study the synchronization problem: all clocks must eventually reach equal values modulo some given positive integer P, despite the arbitrary values of the clocks. We present some scenarios in which this problem is useful. Agents…
No abstract available.
Les voies de signalisation intracellulaire impliquent des cascades d’interaction entre protéines. Chaque cellule peut alors recevoir des signaux, les propager jusqu’à son noyau, puis les intégrer, ce qui, in fine, influe sur son comportement global. Les protéines s’associent entre elles puis modifient la structure spatiale de leurs voisines, ce qui a…
Aimed at applications of our recently developed rule algebra framework to the study of complex systems, we introduce two novel concepts. Consider a complex system specified in the form of a stochastic rewriting system, in terms of its state space, its initial state and its possible random transitions. Our combinatorial…
Biochemical molecules interact through modification and binding reactions, giving raise to a combinatorial number of possible biochemical species. The time-dependent evolution of concentrations of the species is commonly described by a system of coupled ordinary differential equations (ODEs). However, the analysis of such high-dimensional, non-linear system of equations is often…
No abstract available (joint work with Vincent Danos).
