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…
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…
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…
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…
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…
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…
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…
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,…
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…
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.
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…
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…
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…
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…
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…
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.…
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 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,…
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…
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…
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…
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, 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),…
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…
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…
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…
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…
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…
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,…
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…
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.…
