The Antique’s team seminar “SemAntique” takes place every Friday at 2pm, in the team’s office. If you want to be notified of upcoming seminars, do not hesitate to subscribe to the diffusion list.
This seminar is currently managed by Bernadette Charron-Bost and Naïm Moussaoui Remil.
Upcoming events
Archive
2025-2026
-
A Compositional Semantics of Assignment — or, L-values Demystified and Deprecated
In Fortran/Algol tradition, a mutable variable is a variable that can be directly mutated as such by assignment, increment, etc. In contrast, ML tradition uses variables of reference types, bound to ‘boxed values’, or reference cells. These are ordinary, lambda-calculus variables that can be substituted for but not mutated…
-
Reachability Analysis for Parametric Rule-Based Models
Biological system modeling is an iterative process where uncertainties may arise, especially in the early stages of the modeling. Static analysis tools are needed during each stage of the modeling to help modelers detect unexpected behaviors early by automatically inferring properties about the model. However, the rule-based modeling language Kappa…
2024-2025
-
The Heard-Of model: computing in distributed systems with benign faults
Problems in fault-tolerant distributed computing have been studied in a variety of models, structured around two central ideas: (1) degree of synchrony and failure model are two independent parameters, and (2) the origin of faults, i.e., the faulty components (process or channels), must be reported. In this work, we question…
-
Braids, Twists, Trace and Duality in Combinatory Algebras
From the lambda calculus and (some of) its “classic” graphical representations developed by Zeilberger, Hasegawa introduced a new lambda calculus, the “braided lambda calculus”, that keeps track of some geometrical interactions appearing naturally in Zeilberger’s work. From the braided lambda calculus, he developed a sound and complete axiomatization of various…
-
Using Hybrid Contrained Zonotopes to scale abstract domains to Large Language Models
Zonotopes are promising abstract domains for machine learning oriented tasks due to their efficiency, but they fail to capture complex transformations needed in new architectures, like the softmax, used in the attention mechanism of Large Language Models. While recent work proposed more precise Zonotopes, like Polynomial Zonotopes or Hybrid Constrained…
-
Mathematical Informatics
Traditional computability theory does not fully capture the essence of computation. It focuses on what can be computed, neglecting how things are computed. I will present a mathematization of computer science fundamental notions, grounded in the theory of dynamical systems, which prioritizes the ‘how’ over the ‘what’. This approach has…
-
Polymorphic Reachability Types and Effects: An Overview
Fueled by the success of Rust, many programming languages are adding substructural features to their type systems. The promise of tracking properties such as lifetimes and sharing is tremendous, not just for low-level memory management, but also for controlling higher-level resources and capabilities. But so are the difficulties in adapting…
-
Higher-Order Bayesian Networks, Exactly
Bayesian networks (BNs) are graphical first-order probabilistic models that allow for a compact representation of large probability distributions, and efficient inference, both exact and approximate. We introduce a higher-order programming language, in the idealized form of a lambda-calculus, which we prove sound and complete w.r.t. BNs: each BN can be…
-
Coma, an Intermediate Verification Language with Explicit Abstraction Barriers
We introduce Coma, a formally defined intermediate verification language. Specification annotations in Coma take the form of assertions mixed with the executable program code. A special programming construct representing the abstraction barrier is used to separate, inside a subroutine, the “interface” part of the code, which is verified at every…
-
A compositional approach to Taylor expansion
The combination of the theory of differential calculus with the theory of programming languages is an active field of research, with the development of automated differentiation and of the differential lambda calculus. It is well known that differentiation can be turned into a compositional operation, using the tangent bundle construction,…
-
Abstract Lipschitz Continuity
In this seminar, I will introduce Abstract Lipschitz Continuity (ALC), a generalization of the standard Lipschitz continuity notion. While traditional Lipschitz continuity is defined over metric spaces, ALC extends this notion to pre-metric spaces with a partial ordering, ensuring that small variations in the semantic approximations of inputs lead to…
-
Termination resilience static analysis
In this presentation I will present a static analysis proving Termination Resilience of programs i.e. the absence of Robust Non-Termination vulnerabilities in software systems. Robust Non-Termination characterizes programs where an externally-controlled input can force infinite execution, independently of other uncontrolled variables.
-
Abstraction of memory block manipulations by symbolic loop folding
We introduce a new abstract domain for analyzing memory block manipulations, focusing on programs with dynamically allocated arrays. This domain computes properties universally quantified over the value of the loop counters, both for assignments and tests. These properties consist of equalities and comparison predicates involving abstract expressions, represented as affine…
-
Synchronous Programming with Refinement Types
This talk will present MARVeLus, a cyber-physical systems language which combines verification, simulation, and implementation. The language is based on Zélus, a modern version of Lustre, where we add refinement types and associated typing rules. Our refinement types can express temporal-logic-based safety properties and prove them using a rich type…
-
Generable Properties in Abstract Interpretation
The essence of abstract interpretation lies in the use of a simplified domain of abstract properties, known as the abstract domain, which enables the proof of properties about the concrete semantics of programs in a computationally feasible manner. In this seminar, I will demonstrate that certain elements within the concrete…
-
Coinductive Proofs for Temporal Hyperliveness
Temporal logics for hyperproperties have recently emerged as an expressive specification technique for relational properties of reactive systems. While the model checking problem for such logics has been widely studied, there is a scarcity of deductive proof systems for temporal hyperproperties. In particular, hyperproperties with an alternation of universal and…
-
Type Checking is Proof Reductions in Classical Linear Logic
In this talk, I will try to convince you that type checking can be seen as logic programs with a fine-grained input-output system, and query evaluations are proof reductions in classical linear logic. This gives us implementations of type checking algorithms for free, via direct translation from bidirectional typing rules…
-
My initiation to abstract interpretation with the Karr domain
In order to discover abstract interpretation, I implemented a well-known numerical abstract domain in the static analyzer MemCAD. This domain, described in 1974 by Karr, can infer affine equalities of the shape “aX + bY + … = c”. Such properties are helpful to develop optimizing compilers and static analyzers.…
-
Osiris: towards formal semantics and reasoning for OCaml
I will describe work in progress on Osiris, an attempt to equip a nontrivial fragment of OCaml with a formal semantics and with an interactive program verification environment, hosted inside the Rocq proof assistant. Our semantics is hybrid: it takes the form of a monadic interpreter, defined on top of…
-
C-2PO: A Weakly-Relational Pointer Analysis for the Goblint Abstract Interpreter
C is widely used in safety-critical systems, therefore it is important to have static analysis tools that can automatically identify program properties and thus help in the search for bugs. I will present C-2PO, a weakly-relational pointer analysis that can infer relationships between pairs of pointer terms in C programs,…
-
A Causality Analysis for Synchronous Languages
The causality in synchronous languages is a very old problem, used to produce modular scheduled imperative code, for which many answers have already been given. Interestingly, starting from a state-based semantics for a Lustre-like language, I will present how the causality could be used to ease the static analysis of…
-
Une sémantique dénotationnelle pour un compilateur synchrone vérifié
Nous encodons dans Coq un modèle dénotationnel du langage d’entrée de Vélus, compilateur synchrone vérifié. Nous spécifions formellement les conditions de son équivalence avec le modèle relationnel existant, et nous explorons la possibilité d’un raisonnement interactif sur les programmes, à l’aide notamment d’un plongement du nouveau modèle dans celui des…
-
A scalable framework for backward bounded static symbolic execution
Many programs (e.g. malware) hide their behavior by using obfuscations such as opaque predicates. Automatic methods have been developed to detect such obfuscations. In this presentation, we will focus on static symbolic backward bounded execution, a method that enumerates backward bounded paths from a potential opaque predicate and uses symbolic…
-
Compiling with abstract interpretation
Software analyzers and compilers have a lot in common: they both have to read and understand source code in order to prove facts about it and transform it into an equivalent code. While the goal of an analyzer is to prove facts (correctness, safety…) about the source, it often transforms…
-
Consensus = “Stay Safe” + “Try, and Retry again”
Consensus, also known as Byzantine Agreement, has been extensively studied across various models, each characterized by different assumptions regarding cryptographic setups (such as private channels, public key infrastructure, hash functions, or common random strings), network synchrony (synchronous, partially synchronous, fully asynchronous), adversary capabilities (degree of adaptiveness, rushing behavior, computational limits),…
-
Metropolis algorithm in distributed computing
I will present the general notion of (weighted) averaging algorithms and the particular Metropolis algorithm which achieves consensus on the average of initial values in the case of networks with bidirectional communication links. This algorithm converges in quadratic time, even in the case of a dynamic network but, unfortunately, requires…
-
Towards a High Level Linter for Data Science
Due to its interdisciplinary nature, the development of data science code is subject to a wide range of potential mistakes that can easily compromise the final results. Several tools have been proposed that can help the data scientist in identifying the most common, low level programming issues. We discuss the…
-
Metaprogramming Program Analyzers
In this talk, I will talk about how metaprogramming techniques can help build correct, flexible, and performant program analyzers. Metaprogramming techniques manipulate and transform programs as data objects. By considering static program analyzers as the objects to be manipulated or transformed, I will demonstrate how these techniques improve the construction…
-
Protocol Engineering at Informal Systems
Informal systems is one of the stewards of the open-source software of the Cosmos blockchain ecosystem. For instance, we are stewarding CometBFT, a state machine replication engine around Tendermint consensus. In addition, Informal is collaborating with other companies on the design and implementation of distributed systems and algorithms. In this…
-
A Generic Methodology for Statically Analyzing Distributed Architectures: From Robotics to Microservices
Sound static analysis allows one to overapproximate all possible program executions to infer various properties. However, it requires quite some effort to formalize and prove the soundness of program semantics. Most software applications developed nowadays are distributed systems in which different computational entities communicate through synchronous and asynchronous mechanisms. These…
-
OptiTrust: Producing Trustworthy High-Performance Code via Source-to-Source Transformations
Developments in hardware have delivered formidable computing power. Yet, the increased hardware complexity has made it a real challenge to develop software that exploits hardware to its full potential. Numerous approaches have been explored to help programmers turn naive code into high-performance code, finely tuned for the targeted hardware. However,…
-
Easing implementation and maintenance of academic static analyzers
Academic research in static analysis produces software implementations. These implementations are time-consuming to develop and to maintain, in order to enable building further research upon the implementation. While necessary, these processes can be quickly time-consuming. This work documents the tools and techniques we have come up with to simplify the…
-
Automatic verification of tasks schedulers
The aim of this thesis is the verification of task schedulers for operating systems through static analysis based on abstract interpretation. Operating systems are collections of software present on almost every computer. Their purpose is to allow other programs to run without having to manage low-level problems such as memory.…
2023-2024
-
Scheduling and compiling rate-synchronous programs with end-to-end latency constraints
Embedded control software is often specified as a set of periodic tasks together with a dependency graph describing their communications via shared variables. This talk will describe an ongoing collaboration with Airbus to express such systems in a specialized version of Lustre. This version of Lustre is “rate synchronous” in…
-
Analyse statique de valeurs par interprétation abstraite de langages fonctionnels
Dans cette présentation, je vous parlerai de mes travaux sur l’analyse de valeurs par interprétation abstraite des langages fonctionnels.Nos premiers résultats, basés sur des domaines abstraits relationnels et des résumés des champs récursifs des types algébriques, permettent d’analyser des fonctions récursives du premier ordre manipulant des types algébriques récursifs et…
-
A space tale from the (separating) stars
Garbage collection greatly simplifies the life of the programmer, removing the need for manually deallocating memory. However, heap space usage of garbage-collected programs can be tricky to understand: to argue that the garbage collector can reclaim the space associated with a heap object, one has to prove that this object…
-
Static analysis of digital filters
Digital filters are widely used in control/command programs: a digital filter is a numerical algorithm to smooth variations of sampled values of signal. Digital filters involve linear recursions that can hardly be bound by using linear invariants. We propose an abstract domain using quadratic constraints and formal expansion to bound…
-
Introduction to Kalman filters
We consider a certain dynamic system, that is, a system with a certain internal state whose evolution is ruled by a known state update function. At regular interval, a measurement is performed. Based on this series of measurements, our objective is obtaining a good estimation of the current state of…
-
Abstract heap relations for a compositional shape analysis
Static analyses aim at inferring semantic properties of programs. We distinguish two important classes of static analyses: state analyses and relational analyses. While state analyses aim at computing an over-approximation of reachable states of programs, relational analyses aim at computing functional properties over the input-output states of programs. Relational analyses…
-
Sound Static Analysis of Regular Expressions for Vulnerabilities to Denial of Service Attacks
Modern programming languages often provide functions to manipulate regular expressions in standard libraries.If they offer support for advanced features, the matching algorithm has an exponential worst-case time complexity: for some so-called vulnerable regular expressions, an attacker can craft ad hoc strings to force the matcher to exhibit an exponential behaviour…
-
Know your audience! (Cont’d)
In the second part of the talk, we tackle the setting of dynamic networks and present a quite different approach for the distributed computation of functions, which is based on popular algorithms in statistical physics, namely the Metropolis algorithm and the Push-Sum algorithm. When an upper bound on the network…
-
Know your audience!
In this talk, we present several results on distributed function computation in anonymous network with broadcast communications. First, we recall the characterization, given by Boldi and Vigna, of the computable functions when agents have no information on their outgoing neighborhoods. Then we characterize the class of computable functions in networks…
-
Towards Rezk Completion for Higher Categorical Structures
When studying categories in homotopy type theory, it turns out that the well-behaved definition is that of univalent categories, that is, categories such that isomorphisms between objects are equivalent to identities between them. It has been shown that any category is weakly equivalent to a univalent one; this operation is…
-
Automatic Detection of Vulnerable Variables for CTL Properties of Programs
Violations of program properties pose significant risks, particularly when they can be triggered by attackers. Multiple approaches has been proposed recently to detect these vulnerabilities. In this seminar, we will present a new abstract interpretation-based static analysis for this problem. By leveraging a static analysis by abstract interpretation for CTL…
-
Cryptographic Reductions By Bi-Deduction
In this presentation, we are interested in the Computationally Complete Symbolic Attack (CCSA) approach to security protocol verification, and its implementation in the proof assistant SQUIRREL. The proof of a protocol relies on assumptions on the security provided by its primitives (e.g. hash, encryption, etc.), which are generally formulated in…
-
SSA Translation Is an Abstract Interpretation, and its Application to Static Analysis of Machine Code
Conversion to Static Single Assignment (SSA) form is usually viewed as a syntactic transformation algorithm that gives unique names to program variables, and reconciles these names using “phi” functions based on a notion of domination. We instead propose a semantic approach, where SSA translation is performed using a simple dataflow…
-
Investigating the finite-cliquewidth-model property of C²
I will present the work I did during my M1 internship in Dresden on two-variable logics (especially C², the two variable first-order logic with counting quantifiers), trying to show that every satisfiable sentence admits a model of finite cliquewidth.
-
The impossibility result of Fischer, Lynch, and Paterson and its proof
One of the most important results in distributed computing was published in April 1985 by Fischer, Lynch and Paterson. Their short paper “Impossibility of Distributed Consensus with One Faulty Process” definitively placed an upper bound on what it is possible to achieve with distributed processes in an asynchronous environment. The problem of…
-
Probabilistic programming and denotational semantics
Probabilistic programming is a method for Bayesian statistics in which statistical models are encoded as programs. In this talk I will introduce probabilistic programming and the problem of inference. I will then present two kinds of semantics for probabilistic programs: one based on measures and probability kernels, and one based…
-
Monotonicity and the Precision of Program Analysis
It is widely known that the precision of a program analyzer is closely related to intensional program properties, namely, properties concerning how the program is written. This explains, for instance, the interest in code obfuscation techniques, namely, tools explicitly designed to degrade the results of program analysis by operating syntactic…
-
Automatic Inference of Ranking Functions by Abstract Interpretation
We present an abstract interpretation framework for proving liveness properties of imperative programs, to ensure that some event happens once or infinitely many times during program execution. A further abstraction based on piecewise-defined ranking functions yields a static analysis that automatically infers sufficient conditions for these liveness properties as well as upper…
-
From Neural Network Verification to Efficient Robust Training
Fundamental concerns exist on the trustworthiness of deep learning systems, with examples including robustness, fairness, privacy and explainability. Phenomena like adversarial examples prompt the need to train robust networks and to provide formal guarantees on their behaviour. In this talk, we will first introduce the neural network verification problem. Then,…
-
Compositional shape analysis by means of bi-abduction
We present the article “Shape analysis by means of bi-abduction” by Cristiano Calcagno, Dino Distefano, Peter O’Hearn, Hongseok Yang published at POPL in 2009. This article addresses the problem of pre- & post-condition generation and verification for function analysis. In order to resolve this problem, the authors introduce the notion…
-
Thesis rehearsal: “Faithful Model Reduction of Discrete Biological Systems”
Modeling paradigms for Systems Biology plays an important role in investigating the orchestrated function of various biological systems. Additionally, they permit one to study a system in-silico in order to gain mechanistic insights from the trajectories resulting from the model. A common battle to derive an ideal representation for a…
-
Enforcing Modular Security through Language Design: A Study on Object and Reference Capabilities
We present an approach to language design aimed at enforcing modular security, where a security architect can define specific object capabilities that enforce custom security properties. Unlike traditional models that assume an uncompromised system (‘clean garden’), this model (‘dark forest’) assumes local machines are already compromised but anchored by a…
-
Sound Abstract Nonexploitability Analysis
Runtime errors that can be triggered by an attacker are sensibly more dangerous than others, as they not only result in program failure, but can also be exploited and lead to security breaches such as Denial-of-Service attacks or remote code execution. Proving the absence of exploitable runtime errors is challenging,…
-
Towards verified inference in probabilistic programs
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…
-
Easy impossibility proofs for consensus
I present two impossibility proofs for consensus in the presence of byzantine failures based on graph coverings.
-
Event structures, CAT(0) cube complexes, and median graphs
Event structures, trace automata, and Petri nets are fundamental models in concurrency theory. There exist nice interpretations of these structures as combinatorial and geometric objects and both conjectures can be reformulated in this framework. Namely, from a graph theoretical point of view, the domains of prime event structures correspond exactly…
-
Analysis of incomplete programs via Proof Engines and Fuzzing
We tackle the problem of testing and verifying “incomplete” programs—that contain components whose source code is either unavailable (like third-party libraries and cloud-based APIs), or too complex to model formally (like large machine learning models). We show how classical techniques like symbolic execution, deductive verification and SMT solving can be…
-
A static analysis by abstract interpretation for Robust CTL
In this work, we propose a static analysis by abstract interpretation for Robust CTL properties by taking advantage of our static analyzer FuncTion. A CTL property robustly hold if a controlled input imply it whatever the value of the uncontrolled input. Furthermore, we enhance Conflict Driven Analysis (CDA), an extension…
2022-2023
-
Symbolic Reasoning in the Era of Deep Learning
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…
-
A Learner-verifier Framework for Learning and Certifying Neural Controllers in Stochastic Systems
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…
-
Under-Approximated Program Analysis and Counter-Example Generation by Abstract Interpretation
The goal of the PhD is to design, prove correct, implement, and experiment on static program analyses to discover executions that are formally guaranteed to be erroneous and, dually, infer sufficient conditions for program correctness. The error is only reported due to over-approximations (so-called false alarm). Backward analyses have been…
-
Towards an Automatic Proof of the Bakery Algorithm
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…
-
A Product of Shape and Sequence Abstractions
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…
-
Probabilistic proofs in distributed systems
We consider a distributed system in which agents communicate by sending messages and operate in synchronous rounds (roughly, all nodes update their internal state at the same frequency). There are many ways to model the communications on a distributed systems using a probabilistic approach. For example, in the PUSH model,…
-
Symmetries in site-graph rewriting and model reduction
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…
-
Computable Functions in Anonymous Networks
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)…
-
Symbolic transformation of expressions in modular arithmetic
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…
-
Sequentialization of Distal programs
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.
-
Distributed Decision Problems: Concurrent Specifications beyond Binary Relations
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…
-
A generic framework to coarse-grain stochastic reaction networks by Abstract Interpretation
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,…
-
A Data Usage analysis of Jupyter Notebook apps using Abstract Inter
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…
-
Quantitative Input Feature Usage
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…
-
Asymptotically Tight Bounds on the Time Complexity of Broadcast and its Variants in Dynamic Networks
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…
-
Partial (In)Completeness in Abstract Interpretation
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.…
-
A Practical Approach for Describing Language Semantics
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…
-
Sound Symbolic Execution via Abstract Interpretation and Its Application to Security
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…
-
Approximation of models of polymers
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…
-
Abstract Interpretation-Based Feature Importance for SVMs
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…
-
Toward proving program manipulating
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…
-
Towards verified inference in probabilistic programs
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…
-
Verifying Asynchronous JavaScript: a Backward Goal-Directed Approach
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…
-
Clock Synchronization in Dynamic Networks
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…
-
Linera: a Blockchain Infrastructure for Highly-Scalable Web3 Applications
No abstract available.
-
Réduction exacte de modèles biochimiques de signalisation intercellulaire
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…
2018-2019
-
Combinatorial Conversion and Moment Bisimulation for Stochastic Rewriting Systems
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…
-
Tropical Abstraction of Biochemical Reaction Networks with Guarantees
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…
-
A weak consensus algorithm with applications to sidechaining
No abstract available (joint work with Vincent Danos).
