In this talk, we will show how one can augment classes of Boolean
circuits used in knowledge compilation so that one can efficiently check that
they are equivalent to a given CNF formula. We will show that it can be applied
to define Cook-Reckhow proof systems for #SAT and maxSAT and how one can use
this idea to output certificates from existing tools solving #SAT.

Un grand nombre d’automates cellulaires ont été donnés sous forme de table de transition construite à la main. La méthodologie des “champs cellulaires” donne les principes de conception modulaire et de génération de la table de transition en dernière étape, comme c’est le cas pour le code source d’un langage de programmation de haut niveau et leur fichier exécutable binaire. Nous vérifions si les tables ainsi générées peuvent être optimisées pour être aussi petites que leurs contreparties construites à la main. Ceci est fait dans le cas particulier d’un automate cellulaire qui résout le problème de synchronisation des fusiliers (Firing Squad Synchronization problem en anglais) en utilisant des champs cellulaires. Nous étudions la structure interne de cette solution et ainsi que des notions de réduction dans la même veine que la minimisation des automates finis déterministe. La comparaison est faite avec la solution “à la main” de Noguchi.

The valued constraint satisfaction problem (VCSP) is a framework for describing and studying many classes of discrete optimisation problems. It is an optimisation version of the constraint satisfaction problem (CSP), where the goal is to decide whether one can assign labels to variables under some given set of constraints. The VCSP captures both Max CSP-type problems, where one wants to optimise the number of satisfied constraints, and integer programming-type problems, where one adds an objective function to an ordinary CSP to indicate the desirability of each solution.

I will talk about algorithms and hardness results for VCSPs where we restrict the types of cost functions that are allowed to appear in the description of an instance. The algorithms that I consider are based on linear programming (LP), in particular LP relaxations in the Sherali-Adams hierarchy. It turns out that for large classes of VCSPs, there is a complete dichotomy between problems that can be solved by this type of algorithm and problems that can encode NP-hard problems.

Les sous-shifts sont des coloriages de $\mathbb{Z}^d$ verifiant des contraintes locales. Très tôt l’étude de sous-shifts en dimension supérieure à 2 a vu deux notions apparaître naturellement : l’apériodicité et l’indécidabilité. Nous explorons ces deux notions dans ce manuscrit, la seconde par le prisme de différentes notions de complexité, puis nous introduisons un nouveau regard sur les sous-shifts par le biais d’analogies avec la théorie des groupes.

Les sous-shifts sans point périodique, dits apériodiques, ont fait leur apparition avec la construction de Berger prouvant l’indécidabilité de la pavabilité du plan avec le formalisme des tuiles de Wang. Les sous-shifts apériodiques
ont ensuite été l’ingrédient principal de la plupart des constructions. Dans ce document nous nous intéressons
à la notion duale qui consiste à contenir un point apériodique. Nous montrons que les sous-shifts contenant un
point apériodique en contiennent toujours avec une apériodicité régulière : dans des boules concentriques
dont le rayon ne dépend que de la période.

La complexité dans les sous-shifts peut prendre plusieurs formes. Nous illustrons ici les différents liens qui unissent certaines de ces notions de complexité : complexité de Kolmogorov, complexité des configurations via le spectre des degrés Turing, ainsi que complexité au sens du nombre de motifs.

Nous introduisons en fin de manuscrit des analogies avec la théorie des groupes qui nous permettent d’énoncer
des analogues aux théorèmes de Higman dans le cadre des sous-shifts.

This work is concerned with validation of cyber-physical systems (CPS) via simulation based on sampling of the input signal space. Such a space is infinite and in general too difficult to treat symbolically meaning that the only reasonable option is to sample a finite subset of it and simulate the corresponding system behaviours. It is thus of great interest to choose a finite sample so that it best “covers” the whole space of input signals. We use timed automata to model temporal constraints, in order to avoid spurious bugs coming from unrealistic inputs and this can also reduce the input space to explore. We propose a method for low discrepancy generation of signals with temporal constraints recognised by timed automata. The discrepancy notion reflects how uniform the input signal space is sampled and additionally allows deriving validation and performance guarantees. We also show how this notion can be used to measure the discrepancy of a given set of input signals. We describe a prototype tool chain and demonstrate the proposed methods on a Kinetic Battery Model (KiBaM) and a Sigma Delta modulator.

Debug information, usually encoded in the DWARF format, is a hidden and obscure component of our computing infrastructure. Debug information is obviously used by debuggers, but it also plays a key role in program analysis tools, and, most surprisingly, it can be relied upon by the runtime of high-level programming languages. For instance the C++ runtime leverages DWARF stack unwind tables to implement exceptions! Alas, generating debug information adds significant burden to compiler implementations, and the debug information itself can be pervaded by subtle bugs, making the whole infrastructure unreliable. Additionally, interpreting the debug tables is time consuming and for applications as sampling profilers it is a performance bottle-neck.

In this talk I will focus on the DWARF unwind table, that enables stack unwinding in absence of frame-pointer information. I will describe two techniques to perform validation and synthesis of the DWARF stack unwinding tables, and their implementation for the x86_64 architecture. The validation tool has proven effective for compiler and inline assembly testing, while the synthesis tool can generate DWARF unwind tables for arbitrary binaries lacking debug information. Additionally, I will report on a technique to precompile unwind tables into native x86_64 code, which we have implemented and integrated into libunwind, resulting in a 25x DWARF-based unwind speedup.